namespace http://cds.omdoc.org/urtheories

import rules scala://lf.mmt.kwarc.info
rule scala://parser.api.mmt.kwarc.info?MMTURILexer

theory Isabelle =
   include ☞http://cds.omdoc.org/mmt?Errors❚
   include ?PLF
   
   prop: type
   ded : prop ⟶ type  #  1 prec 0

   proof_text: type