Commit f4d7acaf authored by Florian Rabe's avatar Florian Rabe

no message

parent d09e2afa
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/urtheories/lf.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#0.0.0:1991.96.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://cds.omdoc.org/urtheories"/><instruction text="import meta http://cds.omdoc.org/mmt"/><instruction text="import rules scala://lf.mmt.kwarc.info"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><mref name="[http://cds.omdoc.org/urtheories?Typed]" target="http://cds.omdoc.org/urtheories?Typed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#176.7.0:187.7.11"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?Kinded]" target="http://cds.omdoc.org/urtheories?Kinded"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#447.17.0:459.17.12"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?TypedConstants]" target="http://cds.omdoc.org/urtheories?TypedConstants"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#496.22.0:516.22.20"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?KindedConstants]" target="http://cds.omdoc.org/urtheories?KindedConstants"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#582.27.0:603.27.21"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?TermsTypesKinds]" target="http://cds.omdoc.org/urtheories?TermsTypesKinds"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#669.32.0:690.32.21"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LambdaPi]" target="http://cds.omdoc.org/urtheories?LambdaPi"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#959.45.0:973.45.14"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LFRules]" target="http://cds.omdoc.org/urtheories?LFRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1148.53.0:1161.53.13"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LF]" target="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1708.79.0:1716.79.8"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?ShallowPolymorphism]" target="http://cds.omdoc.org/urtheories?ShallowPolymorphism"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1798.85.0:1823.85.25"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?PLF]" target="http://cds.omdoc.org/urtheories?PLF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1927.92.0:1936.92.9"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/urtheories/lf.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#0.0.0:1930.95.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://cds.omdoc.org/urtheories"/><instruction text="import meta http://cds.omdoc.org/mmt"/><instruction text="import rules scala://lf.mmt.kwarc.info"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><mref name="[http://cds.omdoc.org/urtheories?Typed]" target="http://cds.omdoc.org/urtheories?Typed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#176.7.0:187.7.11"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?Kinded]" target="http://cds.omdoc.org/urtheories?Kinded"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#386.16.0:398.16.12"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?TypedConstants]" target="http://cds.omdoc.org/urtheories?TypedConstants"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#435.21.0:455.21.20"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?KindedConstants]" target="http://cds.omdoc.org/urtheories?KindedConstants"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#521.26.0:542.26.21"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?TermsTypesKinds]" target="http://cds.omdoc.org/urtheories?TermsTypesKinds"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#608.31.0:629.31.21"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LambdaPi]" target="http://cds.omdoc.org/urtheories?LambdaPi"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#898.44.0:912.44.14"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LFRules]" target="http://cds.omdoc.org/urtheories?LFRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1087.52.0:1100.52.13"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LF]" target="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1647.78.0:1655.78.8"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?ShallowPolymorphism]" target="http://cds.omdoc.org/urtheories?ShallowPolymorphism"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1737.84.0:1762.84.25"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?PLF]" target="http://cds.omdoc.org/urtheories?PLF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/lf.mmt#1866.91.0:1875.91.9"/></metadata></mref></omdoc>
\ No newline at end of file
theory http://cds.omdoc.org/urtheories?LFRules
Includes http://cds.omdoc.org/urtheories?LFRules http://cds.omdoc.org/urtheories?LambdaPi
Includes http://cds.omdoc.org/urtheories?LFRules http://cds.omdoc.org/urtheories?Kinded
Includes http://cds.omdoc.org/urtheories?LFRules http://cds.omdoc.org/urtheories?Typed
Declares http://cds.omdoc.org/urtheories?LFRules http://cds.omdoc.org/urtheories?LFRules?[scala://lf.mmt.kwarc.info?PiType]
constant http://cds.omdoc.org/urtheories?LFRules?[scala://lf.mmt.kwarc.info?PiType]
Declares http://cds.omdoc.org/urtheories?LFRules http://cds.omdoc.org/urtheories?LFRules?[scala://lf.mmt.kwarc.info?PiTerm]
......
theory http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?TermsTypesKinds
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/mmt?Errors
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?ModExp
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/mmt?mmt
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?Typed
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?Kinded
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?TypedConstants
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?KindedConstants
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?LambdaPi
Includes http://cds.omdoc.org/urtheories?LF http://cds.omdoc.org/urtheories?LFRules
......@@ -4,7 +4,6 @@ untypedconstant http://cds.omdoc.org/urtheories?LambdaPi?apply
untypedconstant http://cds.omdoc.org/urtheories?LambdaPi?arrow
theory http://cds.omdoc.org/urtheories?LambdaPi
Includes http://cds.omdoc.org/urtheories?LambdaPi http://cds.omdoc.org/urtheories?Kinded
Includes http://cds.omdoc.org/urtheories?LambdaPi http://cds.omdoc.org/urtheories?Typed
Declares http://cds.omdoc.org/urtheories?LambdaPi http://cds.omdoc.org/urtheories?LambdaPi?Pi
constant http://cds.omdoc.org/urtheories?LambdaPi?Pi
Declares http://cds.omdoc.org/urtheories?LambdaPi http://cds.omdoc.org/urtheories?LambdaPi?lambda
......
theory http://cds.omdoc.org/urtheories?PLF
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?TermsTypesKinds
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/mmt?Errors
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?ModExp
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/mmt?mmt
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?Typed
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?Kinded
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?TypedConstants
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?KindedConstants
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?LambdaPi
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?LFRules
Includes http://cds.omdoc.org/urtheories?PLF http://cds.omdoc.org/urtheories?ShallowPolymorphism
untypedconstant http://cds.omdoc.org/urtheories?Typed?type
untypedconstant http://cds.omdoc.org/urtheories?Typed?oftype
untypedconstant http://cds.omdoc.org/urtheories?Typed?equality
untypedconstant http://cds.omdoc.org/urtheories?Typed?typeAttribution
untypedconstant http://cds.omdoc.org/urtheories?Typed?defAttribution
untypedconstant http://cds.omdoc.org/urtheories?Typed?notationAttribution
untypedconstant http://cds.omdoc.org/urtheories?Typed?oftype
untypedconstant http://cds.omdoc.org/urtheories?Typed?definedas
untypedconstant http://cds.omdoc.org/urtheories?Typed?withnotation
theory http://cds.omdoc.org/urtheories?Typed
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?type
constant http://cds.omdoc.org/urtheories?Typed?type
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?oftype
constant http://cds.omdoc.org/urtheories?Typed?oftype
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?equality
constant http://cds.omdoc.org/urtheories?Typed?equality
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?typeAttribution
constant http://cds.omdoc.org/urtheories?Typed?typeAttribution
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?defAttribution
constant http://cds.omdoc.org/urtheories?Typed?defAttribution
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?notationAttribution
constant http://cds.omdoc.org/urtheories?Typed?notationAttribution
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?oftype
constant http://cds.omdoc.org/urtheories?Typed?oftype
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?definedas
constant http://cds.omdoc.org/urtheories?Typed?definedas
Declares http://cds.omdoc.org/urtheories?Typed http://cds.omdoc.org/urtheories?Typed?withnotation
constant http://cds.omdoc.org/urtheories?Typed?withnotation
......@@ -7,12 +7,11 @@ rule scala://parser.api.mmt.kwarc.info?MMTURILexer❚
theory Typed =
type❙
oftype # : 1 prec -9995❙
equality # equality 1 2 ❘ role Eq❙
typeAttribution # 1 : 2 prec -9997 ❘ role OMLType❙
defAttribution # 1 := 2 prec -9998 ❘ role OMLDef❙
notationAttribution # 1 # 2 prec -9998 ❘ role OMLNotation❙
oftype # 1 : 2 prec -9997 ❘ role Type❙
definedas # 1 := 2 prec -9998 ❘ role Def❙
withnotation # 1 # 2 prec -9998 ❘ role Notation❙
theory Kinded =
......
......@@ -10,7 +10,7 @@ theory ModExp =
constant morphism # MOR 1 2❙
constant diagram # DIAG ❙
complextheory # {| %BL1T,… |} prec -1000005❙
complextheory # block {| L1T,… |} prec -1000005❙
complexmorphism # [| L1D,… |] prec -1000005❙
identity # IDENTITY 1 prec -1❙
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment