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❙
❚