Commit 1e63144c authored by Dennis Müller's avatar Dennis Müller

generated files

parent b56495ca
errors
\ No newline at end of file
errors
*~
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Bool" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#42.2.0:142.6.0"/></metadata><constant name="bool">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#95.3.2:107.3.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Bool" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#42.2.0:142.6.0"/></metadata><constant name="bool">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#95.3.2:107.3.14"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#103.3.10:106.3.13"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="true">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#111.4.2:123.4.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#111.4.2:123.4.14"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Bool" name="bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#119.4.10:122.4.13"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="false">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#127.5.2:140.5.15"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#127.5.2:140.5.15"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Bool" name="bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#136.5.11:139.5.14"/></metadata></om:OMS></om:OMOBJ></type>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Equality" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?PLF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#99.3.0:557.13.0"/></metadata><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#157.4.2:202.4.47"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Equality" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?PLF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#99.3.0:557.13.0"/></metadata><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#157.4.2:202.4.47"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#165.4.10:185.4.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#166.4.11:166.4.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -11,7 +11,7 @@
<notations><notation dimension="1" precedence="50" fixity="mixfix" arguments="2 = 3"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="refl">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#206.5.2:239.5.35"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#206.5.2:239.5.35"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#214.5.10:226.5.22"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="a"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#215.5.11:215.5.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#217.5.13:217.5.13"/></metadata><type><om:OMV name="a"></om:OMV></type></om:OMV></om:OMBVAR>
......@@ -23,7 +23,7 @@
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="refl 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="cong">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#243.6.2:304.6.63"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#243.6.2:304.6.63"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#251.6.10:292.6.51"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="a"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#252.6.11:252.6.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV><om:OMV name="b"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#254.6.13:254.6.13"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#256.6.15:256.6.15"/></metadata><type><om:OMV name="a"></om:OMV></type></om:OMV><om:OMV name="y"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#258.6.17:258.6.17"/></metadata><type><om:OMV name="a"></om:OMV></type></om:OMV></om:OMBVAR>
......@@ -54,7 +54,7 @@
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="cong 5 6"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="cast">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#308.7.2:366.7.60"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#308.7.2:366.7.60"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#316.7.10:365.7.59"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#317.7.11:317.7.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#320.7.14:323.7.17"/></metadata></om:OMS></type></om:OMV><om:OMV name="A"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#326.7.20:326.7.20"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#329.7.23:336.7.30"/></metadata>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLEQNatDed" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#758.26.0:1072.34.0"/></metadata><import from="http://cds.omdoc.org/examples?FOLEQ"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#818.27.2:832.27.16"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://cds.omdoc.org/examples?FOLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#836.28.2:853.28.19"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="refl">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#860.29.2:882.29.24"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLEQNatDed" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#758.26.0:1072.34.0"/></metadata><import from="http://cds.omdoc.org/examples?FOLEQ"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#818.27.2:832.27.16"/></metadata></import><import from="http://cds.omdoc.org/examples?FOLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#836.28.2:853.28.19"/></metadata></import><constant name="refl">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#860.29.2:882.29.24"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#871.29.13:881.29.23"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#872.29.14:872.29.14"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -14,7 +14,7 @@
<notations></notations>
</constant><constant name="congT">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#886.30.2:931.30.47"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#886.30.2:931.30.47"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#897.30.13:930.30.46"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="T"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#898.30.14:898.30.14"/></metadata><type><om:OMBIND>
......@@ -52,7 +52,7 @@
<notations></notations>
</constant><constant name="congF">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#935.31.2:982.31.49"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#935.31.2:982.31.49"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#946.31.13:981.31.48"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="F"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#947.31.14:947.31.14"/></metadata><type><om:OMBIND>
......@@ -90,7 +90,7 @@
<notations></notations>
</constant><constant name="sym">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#986.32.2:1020.32.36"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#986.32.2:1020.32.36"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#997.32.13:1019.32.35"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#998.32.14:998.32.14"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV><om:OMV name="y"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#1000.32.16:1000.32.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -114,7 +114,7 @@
<notations></notations>
</constant><constant name="trans">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#1024.33.2:1070.33.48"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#1024.33.2:1070.33.48"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#1035.33.13:1069.33.47"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#1036.33.14:1036.33.14"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV><om:OMV name="y"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#1038.33.16:1038.33.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV><om:OMV name="z"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#1040.33.18:1040.33.18"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLEQ" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#640.21.0:755.24.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#694.22.2:706.22.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#710.23.2:753.23.45"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLEQ" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#640.21.0:755.24.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#694.22.2:706.22.14"/></metadata></import><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#710.23.2:753.23.45"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#719.23.11:736.23.28"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#733.23.25:736.23.28"/></metadata></om:OMS>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLNatDed" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#319.11.0:637.19.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#377.12.2:389.12.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#393.13.2:409.13.18"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="forallI">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#416.14.2:453.14.39"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLNatDed" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#319.11.0:637.19.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#377.12.2:389.12.14"/></metadata></import><import from="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#393.13.2:409.13.18"/></metadata></import><constant name="forallI">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#416.14.2:453.14.39"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#427.14.13:451.14.37"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="A"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#428.14.14:428.14.14"/></metadata><type><om:OMBIND>
......@@ -31,7 +31,7 @@
<notations></notations>
</constant><constant name="forallE" role="ForwardRule">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#457.15.2:511.15.56"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#457.15.2:511.15.56"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#468.15.13:492.15.37"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="A"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#469.15.14:469.15.14"/></metadata><type><om:OMA>
......@@ -62,7 +62,7 @@
<notations></notations>
</constant><constant name="existsI">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#516.17.2:573.17.59"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#516.17.2:573.17.59"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#527.17.13:557.17.43"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="A"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#528.17.14:528.17.14"/></metadata><type><om:OMBIND>
......@@ -101,7 +101,7 @@
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="existsI 2 3"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="existsE">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#577.18.2:635.18.60"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#577.18.2:635.18.60"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#588.18.13:634.18.59"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="A"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#589.18.14:589.18.14"/></metadata><type><om:OMBIND>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLPatterns" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LFS"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#42.2.0:151.8.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#75.3.2:87.3.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><derived feature="pattern" name="fun" base="http://cds.omdoc.org/examples"><type><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#102.5.10:112.5.20"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLPatterns" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LFS"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#42.2.0:151.8.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#75.3.2:87.3.14"/></metadata></import><derived feature="pattern" name="fun" base="http://cds.omdoc.org/examples"><type><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#102.5.10:112.5.20"/></metadata>
<om:OMS base="scala://patterns.api.mmt.kwarc.info/" module="PatternFeature"></om:OMS>
<om:OMBVAR><om:OMV name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#106.5.14:106.5.14"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#108.5.16:110.5.18"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
</om:OMBIND></type><notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="L1 : 2"> <scope languages="" priority="0"/> </notation></notations><constant name="f">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#129.6.4:145.6.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#129.6.4:145.6.20"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#132.6.7:144.6.19"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#132.6.7:137.6.12"/></metadata>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLProofs" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#501.28.0:754.33.0"/></metadata><import from="http://cds.omdoc.org/examples?FOLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#559.29.2:577.29.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLProofs" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#501.28.0:754.33.0"/></metadata><import from="http://cds.omdoc.org/examples?FOLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#559.29.2:577.29.20"/></metadata></import></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOL" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#135.4.0:316.9.0"/></metadata><import from="http://cds.omdoc.org/examples?PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#187.5.2:198.5.13"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="term">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#202.6.2:214.6.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOL" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#135.4.0:316.9.0"/></metadata><import from="http://cds.omdoc.org/examples?PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#187.5.2:198.5.13"/></metadata></import><constant name="term">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#202.6.2:214.6.14"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#210.6.10:213.6.13"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="forall">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#218.7.2:264.7.48"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#218.7.2:264.7.48"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#227.7.11:246.7.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA>
......@@ -15,7 +15,7 @@
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="∀ 1"> <scope languages="" priority="0"/> </notation><notation dimension="2" precedence="0" fixity="mixfix" arguments="∀ V1 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="exists">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#268.8.2:314.8.48"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#268.8.2:314.8.48"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#277.8.11:296.8.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#277.8.11:289.8.23"/></metadata>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="IntLiterals" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#315.13.0:581.18.0"/></metadata><import from="http://cds.omdoc.org/examples?IntRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#375.14.2:392.14.19"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#500.15.2:518.15.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?StandardInt"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#522.16.2:547.16.27"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="test">
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="IntLiterals" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#315.13.0:581.18.0"/></metadata><import from="http://cds.omdoc.org/examples?IntRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#375.14.2:392.14.19"/></metadata></import><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#500.15.2:518.15.20"/></metadata></import><import from="scala://real.omdoc.org/?StandardInt"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#522.16.2:547.16.27"/></metadata></import><constant name="test">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#551.17.2:579.17.30"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#559.17.10:568.17.19"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Int" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#42.2.0:267.8.0"/></metadata><import from="http://cds.omdoc.org/examples?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#94.3.2:106.3.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="int">
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Int" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#42.2.0:267.8.0"/></metadata><import from="http://cds.omdoc.org/examples?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#94.3.2:106.3.14"/></metadata></import><constant name="int">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#110.4.2:129.4.21"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#118.4.10:121.4.13"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#126.4.18:128.4.20"/></metadata></om:OMS></om:OMOBJ></definition>
</constant><constant name="pred">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#133.5.2:175.5.44"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#133.5.2:175.5.44"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#141.5.10:149.5.18"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#141.5.10:143.5.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#147.5.16:149.5.18"/></metadata></om:OMS>
......@@ -12,7 +12,7 @@
<notations><notation dimension="1" precedence="20" fixity="mixfix" arguments="pred 1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="uminus">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#179.6.2:219.6.42"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#179.6.2:219.6.42"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#187.6.10:195.6.18"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#187.6.10:189.6.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#193.6.16:195.6.18"/></metadata></om:OMS>
......@@ -20,7 +20,7 @@
<notations><notation dimension="1" precedence="20" fixity="mixfix" arguments="- 1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="minus">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#223.7.2:265.7.44"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#223.7.2:265.7.44"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#231.7.10:245.7.24"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#231.7.10:233.7.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#237.7.16:239.7.18"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#243.7.22:245.7.24"/></metadata></om:OMS>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="LFI" base="http://cds.omdoc.org/examples"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#94.4.0:154.7.0"/></metadata><import from="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#110.5.2:124.5.16"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><ruleconstant name="[scala://induction.lf.mmt.kwarc.info?InductiveRule]"><type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="scala://induction.lf.mmt.kwarc.info" module="InductiveRule"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#133.6.7:151.6.25"/></metadata></om:OMS></om:OMOBJ></type></ruleconstant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="LFI" base="http://cds.omdoc.org/examples"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#94.4.0:154.7.0"/></metadata><import from="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#110.5.2:124.5.16"/></metadata></import></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="LFP" base="http://cds.omdoc.org/examples"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#42.2.0:178.6.1"/></metadata><import from="http://cds.omdoc.org/urtheories?LFS"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#57.3.2:73.3.18"/></metadata></import></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Logic" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#145.8.0:286.12.0"/></metadata><import from="http://cds.omdoc.org/examples?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#199.9.2:212.9.15"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="ded" role="Judgment">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#216.10.2:266.10.52"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Logic" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#145.8.0:286.12.0"/></metadata><import from="http://cds.omdoc.org/examples?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#199.9.2:212.9.15"/></metadata></import><constant name="ded" role="Judgment">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#216.10.2:266.10.52"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#224.10.10:234.10.20"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Bool" name="bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#224.10.10:227.10.13"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#231.10.17:234.10.20"/></metadata></om:OMS>
......@@ -7,7 +7,7 @@
<notations><notation dimension="1" precedence="-5" fixity="mixfix" arguments="⊦ 1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="trueI">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#270.11.2:284.11.16"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#270.11.2:284.11.16"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#278.11.10:283.11.15"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Logic" name="ded"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Bool" name="true"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#280.11.12:283.11.15"/></metadata></om:OMS>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="NatExample" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?LFI"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#157.9.0:242.14.2"/></metadata><constant name="inductive">
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="NatExample" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?LFI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#157.9.0:242.14.2"/></metadata><constant name="inductive">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#186.10.2:214.11.11"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#210.11.7:213.11.10"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#207.11.4:213.11.10"/></metadata>
......@@ -10,18 +7,12 @@
</om:OMA></om:OMOBJ></definition>
</constant><constant name="z">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#220.12.4:224.12.8"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#220.12.4:224.12.8"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format="unknown"><![CDATA[n]]></om:text></om:OMSF></om:OMOBJ></type>
</constant><constant name="s">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#230.13.4:238.13.12"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#230.13.4:238.13.12"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#233.13.7:237.13.11"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMSF><om:text format="unknown"><![CDATA[n]]></om:text></om:OMSF><om:OMSF><om:text format="unknown"><![CDATA[n]]></om:text></om:OMSF>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="NatLiterals" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#80.4.0:310.11.0"/></metadata><import from="http://cds.omdoc.org/examples?NatRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#140.5.2:157.5.19"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#161.6.2:179.6.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?StandardNat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#183.7.2:208.7.27"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="test">
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="NatLiterals" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#80.4.0:310.11.0"/></metadata><import from="http://cds.omdoc.org/examples?NatRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#140.5.2:157.5.19"/></metadata></import><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#161.6.2:179.6.20"/></metadata></import><import from="scala://real.omdoc.org/?StandardNat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#183.7.2:208.7.27"/></metadata></import><constant name="test">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#282.10.2:308.10.28"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#290.10.10:298.10.18"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="PLProofs" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#293.19.0:498.26.0"/></metadata><import from="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#350.20.2:367.20.19"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#374.22.2:405.22.33"/></metadata>this doesn't work currently</opaque></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="PLProofs" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#293.19.0:498.26.0"/></metadata><import from="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#350.20.2:367.20.19"/></metadata></import><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#374.22.2:405.22.33"/></metadata>this doesn't work currently</opaque></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="ProgLang" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?CF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#191.6.0:385.13.0"/></metadata><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#248.7.2:266.7.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://cds.omdoc.org/examples?NatRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#270.8.2:287.8.19"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?StandardNat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#291.9.2:316.9.27"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="print">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#323.11.2:360.11.39"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="ProgLang" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?CF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#191.6.0:385.13.0"/></metadata><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#248.7.2:266.7.20"/></metadata></import><import from="http://cds.omdoc.org/examples?NatRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#270.8.2:287.8.19"/></metadata></import><import from="scala://real.omdoc.org/?StandardNat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#291.9.2:316.9.27"/></metadata></import><constant name="print">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#323.11.2:360.11.39"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#331.11.10:348.11.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#332.11.11:332.11.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#335.11.14:338.11.17"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Real" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#216.6.0:490.15.0"/></metadata><constant name="real">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#241.7.2:251.7.12"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Real" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#216.6.0:490.15.0"/></metadata><constant name="real">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#241.7.2:251.7.12"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></type>
</constant><constant name="plus">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#256.9.2:298.9.44"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#256.9.2:298.9.44"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#262.9.8:279.9.25"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#262.9.8:265.9.11"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#269.9.15:272.9.18"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#276.9.22:279.9.25"/></metadata></om:OMS>
......@@ -12,7 +12,7 @@
<notations><notation dimension="1" precedence="10" fixity="mixfix" arguments="1 + 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="minus">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#302.10.2:347.10.47"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#302.10.2:347.10.47"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#310.10.10:327.10.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#310.10.10:313.10.13"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#317.10.17:320.10.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#324.10.24:327.10.27"/></metadata></om:OMS>
......@@ -20,7 +20,7 @@
<notations><notation dimension="1" precedence="10" fixity="mixfix" arguments="1 - 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="times">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#351.11.2:393.11.44"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#351.11.2:393.11.44"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#358.11.9:375.11.26"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#358.11.9:361.11.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#365.11.16:368.11.19"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#372.11.23:375.11.26"/></metadata></om:OMS>
......@@ -28,7 +28,7 @@
<notations><notation dimension="1" precedence="15" fixity="mixfix" arguments="1 * 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="div">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#397.12.2:437.12.42"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#397.12.2:437.12.42"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#402.12.7:419.12.24"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#402.12.7:405.12.10"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#409.12.14:412.12.17"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Real" name="real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#416.12.21:419.12.24"/></metadata></om:OMS>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="RightUnital" base="http://cds.omdoc.org/examples"><definition><om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="unknown"></om:OMS>
<om:OMBVAR><om:OMV name="/LeftUnital/5"></om:OMV><om:OMV name="/VIA/4"></om:OMV><om:OMV name="/Flip/3"></om:OMV><om:OMV name="/RENAME/2"></om:OMV><om:OMV name="/leftIdentity/1"></om:OMV><om:OMV name="/rightIdentity/0"></om:OMV></om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="rightIdentity"><type><om:OMV name="/rightIdentity/0"></om:OMV></type></om:OMV><om:OMV name="leftIdentity"><type><om:OMV name="/leftIdentity/1"></om:OMV></type></om:OMV><om:OMV name="RENAME"><type><om:OMV name="/RENAME/2"></om:OMV></type></om:OMV><om:OMV name="Flip"><type><om:OMV name="/Flip/3"></om:OMV></type></om:OMV><om:OMV name="VIA"><type><om:OMV name="/VIA/4"></om:OMV></type></om:OMV><om:OMV name="LeftUnital"><type><om:OMV name="/LeftUnital/5"></om:OMV></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#699.21.27:757.21.85"/></metadata>
<om:OMSF><om:text format="unknown"><![CDATA[(]]></om:text></om:OMSF>
<om:OMV name="LeftUnital"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#700.21.28:709.21.37"/></metadata></om:OMV><om:OMV name="VIA"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#711.21.39:713.21.41"/></metadata></om:OMV><om:OMV name="Flip"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#715.21.43:718.21.46"/></metadata></om:OMV><om:OMSF><om:text format="unknown"><![CDATA[)]]></om:text></om:OMSF><om:OMV name="RENAME"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#721.21.49:726.21.54"/></metadata></om:OMV><om:OMSF><om:text format="unknown"><![CDATA[{]]></om:text></om:OMSF><om:OMV name="leftIdentity"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#729.21.57:740.21.68"/></metadata></om:OMV><om:OMSF><om:text format="unknown"><![CDATA[=]]></om:text></om:OMSF><om:OMV name="rightIdentity"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#744.21.72:756.21.84"/></metadata></om:OMV><om:OMSF><om:text format="unknown"><![CDATA[}]]></om:text></om:OMSF>
</om:OMA>
</om:OMBIND>
</om:OMBIND></definition><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#673.21.1:762.21.90"/></metadata></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Sums" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2791.77.0:3146.88.0"/></metadata><import from="http://cds.omdoc.org/examples?Numbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2844.78.2:2860.78.18"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="nat">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2865.80.2:2879.80.16"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Sums" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2791.77.0:3146.88.0"/></metadata><import from="http://cds.omdoc.org/examples?Numbers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2844.78.2:2860.78.18"/></metadata></import><constant name="nat">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2865.80.2:2879.80.16"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="sort"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2873.80.10:2876.80.13"/></metadata></om:OMS></om:OMOBJ></type>
......@@ -12,7 +12,7 @@
</om:OMA></om:OMOBJ></definition>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="ℕ"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="incl">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2918.82.2:2969.82.53"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2918.82.2:2969.82.53"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2926.82.10:2930.82.14"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="tmnat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2926.82.10:2926.82.10"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2930.82.14:2930.82.14"/></metadata></om:OMS>
......@@ -20,7 +20,7 @@
<notations><notation dimension="1" precedence="170" fixity="mixfix" arguments="$ 1"> <scope languages="" priority="0"/> </notation><notation dimension="2" precedence="100000000" fixity="mixfix" arguments="1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="sum">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2974.84.2:3066.86.31"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2974.84.2:3066.86.31"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2981.84.9:2999.84.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="tmnat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2981.84.9:2981.84.9"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="tmnat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2985.84.13:2985.84.13"/></metadata></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2989.84.17:2995.84.23"/></metadata>
......@@ -31,7 +31,7 @@
<notations><notation dimension="1" precedence="155" fixity="mixfix" arguments="Σ 1 to 2 3"> <scope languages="" priority="0"/> </notation><notation dimension="2" precedence="155" fixity="mixfix" arguments="Σ __ 1 ^^ 2 3"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="sum_example">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3070.87.2:3144.87.76"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3070.87.2:3144.87.76"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3086.87.18:3142.87.74"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3090.87.22:3142.87.74"/></metadata>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Unital" base="http://cds.omdoc.org/examples"><definition><om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="unknown"></om:OMS>
<om:OMBVAR><om:OMV name="/LeftUnital/2"></om:OMV><om:OMV name="/AND/1"></om:OMV><om:OMV name="/RightUnital/0"></om:OMV></om:OMBVAR>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="RightUnital"><type><om:OMV name="/RightUnital/0"></om:OMV></type></om:OMV><om:OMV name="AND"><type><om:OMV name="/AND/1"></om:OMV></type></om:OMV><om:OMV name="LeftUnital"><type><om:OMV name="/LeftUnital/2"></om:OMV></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#787.23.22:812.23.47"/></metadata>
<om:OMV name="LeftUnital"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#787.23.22:796.23.31"/></metadata></om:OMV>
<om:OMV name="AND"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#798.23.33:800.23.35"/></metadata></om:OMV><om:OMV name="RightUnital"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#802.23.37:812.23.47"/></metadata></om:OMV>
</om:OMA>
</om:OMBIND>
</om:OMBIND></definition><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#766.23.1:817.23.52"/></metadata></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Bool" base="http://cds.omdoc.org/examples/ijcar" meta="http://cds.omdoc.org/urtheories?LF"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#360.14.0:444.17.0"/></metadata><constant name="bool">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#395.15.2:405.15.12"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Bool" base="http://cds.omdoc.org/examples/ijcar" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#360.14.0:444.17.0"/></metadata><constant name="bool">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#395.15.2:405.15.12"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#401.15.8:404.15.11"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="proof">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#409.16.2:442.16.35"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#409.16.2:442.16.35"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#416.16.9:426.16.19"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/ijcar" module="Bool" name="bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#416.16.9:419.16.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#423.16.16:426.16.19"/></metadata></om:OMS>
......
This diff is collapsed.
<?xml version="1.0"?>
<locatingRules xmlns="http://thaiopensource.com/ns/locating-rules/1.0">
<uri pattern="*.omdoc" typeId="MMT"/>
<typeId id="MMT" uri="mmt.rnc"/>
</locatingRules>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="AbelianGroup" base="http://cds.omdoc.org/examples/tutorial" meta="http://cds.omdoc.org/examples/tutorial?NatDed"><metadata><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2534.67.0:2604.70.0"/></metadata><import from="http://cds.omdoc.org/examples/tutorial?Group"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2567.68.1:2580.68.14"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import><import from="http://cds.omdoc.org/examples/tutorial?Abelian"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2585.69.1:2600.69.16"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata></import></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="AbelianGroup" base="http://cds.omdoc.org/examples/tutorial" meta="http://cds.omdoc.org/examples/tutorial?NatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2534.67.0:2604.70.0"/></metadata><import from="http://cds.omdoc.org/examples/tutorial?Group"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2567.68.1:2580.68.14"/></metadata></import><import from="http://cds.omdoc.org/examples/tutorial?Abelian"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2585.69.1:2600.69.16"/></metadata></import></theory></omdoc>
\ No newline at end of file