Commit 692b28a9 authored by Florian Rabe's avatar Florian Rabe

no message

parent b30e62f1
......@@ -3,6 +3,7 @@
<classpathentry kind="src" path="scala_realizations"/>
<classpathentry kind="src" path="export/lf-scala"/>
<classpathentry kind="src" path="export/scala"/>
<classpathentry kind="src" path="scala"/>
<classpathentry kind="con" path="org.scala-ide.sdt.launching.SCALA_CONTAINER"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
<classpathentry combineaccessrules="false" kind="src" path="/mmt-api"/>
......
......@@ -92,7 +92,7 @@ end
define temp2
server on 8080
log+ server
log+ debug
//log+ debug
log+ object-checker
//log+ object-simplifier
//log+ structure-simplifier
......@@ -103,8 +103,9 @@ define temp2
//log+ backend
extension info.kwarc.mmt.lf.induction.InductiveTypes
mathpath archive ../../Test/General
//build Test/General mmt-omdoc structures.mmt
build MMT/examples mmt-omdoc inductive.mmt
extension info.kwarc.mmt.odk.Plugin
build MMT/LFX mmt-omdoc
// build MMT/examples mmt-omdoc
end
define MMTTest
......@@ -121,5 +122,6 @@ define MMTTest
mathpath archive ../../Test
mathpath archive ../LFX
mathpath archive ../../MitM
extension info.kwarc.mmt.odk.Plugin
build Test/General mmt-omdoc views.mmt
end
\ No newline at end of file
......@@ -6,7 +6,7 @@
<definition><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#154.5.23:179.5.48"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="Combinators" name="extends"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Algebra/Empty"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#154.5.23:158.5.27"/></metadata></om:OMS><om:OML name="U"><definition><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></definition></om:OML>
<om:OMS base="http://cds.omdoc.org/examples" module="Algebra/Empty"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#154.5.23:158.5.27"/></metadata></om:OMS><om:OML name="U"><definition><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#174.5.43:177.5.46"/></metadata></om:OMS></definition></om:OML>
</om:OMA></definition>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#132.5.1:183.5.52"/></metadata>
</theory><theory name="Magma" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?FOLEQ">
......@@ -39,7 +39,7 @@
<om:OMS base="http://cds.omdoc.org/urtheories" module="Combinators" name="extends"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Algebra/PointedMagma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#394.10.26:405.10.37"/></metadata></om:OMS><om:OML name="leftIdentity"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#431.10.63:454.10.86"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#435.10.67:454.10.86"/></metadata>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="ded"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#431.10.63:433.10.65"/></metadata></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#435.10.67:454.10.86"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="forall"></om:OMS><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#437.10.69:454.10.86"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
......
......@@ -2,7 +2,7 @@
<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>
<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"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#726.23.18:729.23.21"/></metadata></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>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="30" fixity="mixfix" arguments="1 ≐ 2"> <scope languages="" priority="0"/> </notation></notations>
......
......@@ -5,7 +5,14 @@
<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>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="/A/1/v"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><om:OMV name="_"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<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#235.7.19:238.7.22"/></metadata></om:OMS>
</om:OMBIND><om:OMV name="/A/1/v"></om:OMV>
</om:OMA>
</om:OMBIND></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#431.14.17:451.14.37"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
......@@ -36,7 +43,7 @@
<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>
<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="PL" name="prop"></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#235.7.19:238.7.22"/></metadata></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#472.15.17:492.15.37"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
......@@ -68,7 +75,14 @@
<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>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="/A/2/v"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
</om:OMBIND><om:OMV name="/A/2/v"></om:OMV>
</om:OMA>
</om:OMBIND></type></om:OMV></om:OMBVAR>
<om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#531.17.17:557.17.43"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
......@@ -107,7 +121,14 @@
<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>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="/A/2/v"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
</om:OMBIND><om:OMV name="/A/2/v"></om:OMV>
</om:OMA>
</om:OMBIND></type></om:OMV><om:OMV name="C"><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#591.18.16:591.18.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#594.18.19:634.18.59"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
......
......@@ -9,7 +9,7 @@
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA>
<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="PL" name="prop"></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#235.7.19:238.7.22"/></metadata></om:OMS>
</om:OMA><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#243.7.27:246.7.30"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
......
......@@ -95,7 +95,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#564.18.2:619.18.57"/></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/int.mmt#581.18.19:603.18.41"/></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/int.mmt#582.18.20:582.18.20"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/int.mmt#584.18.22:584.18.22"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></om:OMS></type></om:OMV></om:OMBVAR>
<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/int.mmt#582.18.20:582.18.20"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/int.mmt#584.18.22:584.18.22"/></metadata><type><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/nat.mmt#512.20.16:514.20.18"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#587.18.25:603.18.41"/></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:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#589.18.27:603.18.41"/></metadata>
......@@ -116,7 +116,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#623.19.2:678.19.57"/></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/int.mmt#640.19.19:662.19.41"/></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/int.mmt#641.19.20:641.19.20"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/int.mmt#643.19.22:643.19.22"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></om:OMS></type></om:OMV></om:OMBVAR>
<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/int.mmt#641.19.20:641.19.20"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/int.mmt#643.19.22:643.19.22"/></metadata><type><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/nat.mmt#512.20.16:514.20.18"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#646.19.25:662.19.41"/></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:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#648.19.27:662.19.41"/></metadata>
......
<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>
<om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="typeAttribution"></om:OMS>
<om:OMSF><om:text format="unknown"><![CDATA[n]]></om:text></om:OMSF><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:OMA></om:OMOBJ></definition>
<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#158.9.0:246.15.0"/></metadata><derived feature="inductive" name="nat" 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/inductive.mmt#197.10.12:202.10.17"/></metadata>
<om:OMS base="scala://induction.lf.mmt.kwarc.info/" module="InductiveTypes"></om:OMS>
<om:OMBVAR></om:OMBVAR>
</om:OMBIND></type><constant name="n">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#209.11.4:216.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#212.11.7:215.11.10"/></metadata></om:OMS></om:OMOBJ></type>
</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"/></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>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#222.12.4:226.12.8"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="NatExample/nat" name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#225.12.7:225.12.7"/></metadata></om:OMS></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"/></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>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#232.13.4:240.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#235.13.7:239.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>
<om:OMS base="http://cds.omdoc.org/examples" module="NatExample/nat" name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#235.13.7:235.13.7"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="NatExample/nat" name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#239.13.11:239.13.11"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant></theory></omdoc>
\ No newline at end of file
</constant></derived></theory></omdoc>
\ No newline at end of file
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -28,7 +28,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#498.20.2:540.20.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/nat.mmt#506.20.10:520.20.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"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/nat.mmt#518.20.22:520.20.24"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/nat.mmt#512.20.16:514.20.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/nat.mmt#518.20.22:520.20.24"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="10" fixity="mixfix" arguments="1 + 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -36,7 +36,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#544.21.2:586.21.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/nat.mmt#552.21.10:566.21.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"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/nat.mmt#564.21.22:566.21.24"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/nat.mmt#558.21.16:560.21.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/nat.mmt#564.21.22:566.21.24"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="15" fixity="mixfix" arguments="1 * 2"> <scope languages="" priority="0"/> </notation></notations>
......
......@@ -68,7 +68,7 @@
</constant><constant name="tmrat">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#478.15.2:509.15.33"/></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/arithmetic_rules.mmt#486.15.10:489.15.13"/></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/arithmetic_rules.mmt#2930.82.14:2930.82.14"/></metadata>
<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/arithmetic_rules.mmt#496.15.20:501.15.25"/></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="tm"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#496.15.20:497.15.21"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="rat"></om:OMS>
</om:OMA></om:OMOBJ></definition>
......@@ -114,7 +114,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#702.23.2:739.23.39"/></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#709.23.9:717.23.17"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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#717.23.17:717.23.17"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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#713.23.13:713.23.13"/></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#717.23.17:717.23.17"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="150" fixity="mixfix" arguments="1 - 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -168,7 +168,17 @@
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><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/arithmetic_rules.mmt#934.31.26:934.31.26"/></metadata><type><om:OMA>
<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="tm"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMA>
<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="tm"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="rat"></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="rat"></om:OMS>
</om:OMBIND>
<om:OMV name="x"></om:OMV>
</om:OMA>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#936.31.28:953.31.45"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
......@@ -176,7 +186,20 @@
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><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/arithmetic_rules.mmt#937.31.29:937.31.29"/></metadata><type><om:OMA>
<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="tm"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMA>
<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="tm"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="rat"></om:OMS>
</om:OMA></type></om:OMV><om:OMV name="y"><type><om:OMA>
<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="tm"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="rat"></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="rat"></om:OMS>
</om:OMBIND>
<om:OMV name="x"></om:OMV><om:OMV name="y"></om:OMV>
</om:OMA>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#939.31.31:953.31.45"/></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.
......@@ -36,7 +36,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#818.28.2:863.28.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/logic/pl.mmt#826.28.10:843.28.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="PL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#833.28.17:836.28.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="15" fixity="mixfix" arguments="1 ∧ 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -44,7 +44,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#867.29.2:912.29.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/logic/pl.mmt#875.29.10:892.29.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="PL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#889.29.24:892.29.27"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#882.29.17:885.29.20"/></metadata></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/pl.mmt#889.29.24:892.29.27"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="15" fixity="mixfix" arguments="1 ∨ 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -52,7 +52,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#916.30.2:961.30.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/logic/pl.mmt#924.30.10:941.30.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="PL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#938.30.24:941.30.27"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#931.30.17:934.30.20"/></metadata></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/pl.mmt#938.30.24:941.30.27"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="10" fixity="mixfix" arguments="1 ⇒ 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -80,11 +80,11 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1148.34.2:1228.35.33"/></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/pl.mmt#1156.34.10:1173.34.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="PL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#1163.34.17:1166.34.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
</om:OMA></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND>
<definition><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/pl.mmt#1205.35.10:1227.35.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></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/pl.mmt#1206.35.11:1206.35.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#1208.35.13:1208.35.13"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS></type></om:OMV></om:OMBVAR>
<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/pl.mmt#1206.35.11:1206.35.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></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/pl.mmt#1208.35.13:1208.35.13"/></metadata><type><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/pl.mmt#1163.34.17:1166.34.20"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1211.35.16:1227.35.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="and"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1211.35.16:1217.35.22"/></metadata>
......
......@@ -59,11 +59,11 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#257.16.2:288.16.33"/></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/prover.mmt#264.16.9:272.16.17"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="d"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#272.16.17:272.16.17"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#268.16.13:268.16.13"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="d"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#272.16.17:272.16.17"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<definition><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/prover.mmt#278.16.23:287.16.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></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/prover.mmt#279.16.24:279.16.24"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"></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/prover.mmt#281.16.26:281.16.26"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"></om:OMS></type></om:OMV></om:OMBVAR>
<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/prover.mmt#279.16.24:279.16.24"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"></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/prover.mmt#281.16.26:281.16.26"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#268.16.13:268.16.13"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#284.16.29:287.16.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/mmt" module="Errors" name="missing"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="ProverTest" name="d"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#285.16.30:285.16.30"/></metadata></om:OMS>
......
......@@ -388,7 +388,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2098.62.2:2155.62.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/arithmetic_rules.mmt#2112.62.16:2140.62.44"/></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/arithmetic_rules.mmt#2113.62.17:2113.62.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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/arithmetic_rules.mmt#2115.62.19:2115.62.19"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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/arithmetic_rules.mmt#2117.62.21:2117.62.21"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></om:OMS></type></om:OMV></om:OMBVAR>
<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/arithmetic_rules.mmt#2113.62.17:2113.62.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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/arithmetic_rules.mmt#2115.62.19:2115.62.19"/></metadata><type><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#713.23.13:713.23.13"/></metadata></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/arithmetic_rules.mmt#2117.62.21:2117.62.21"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2120.62.24:2140.62.44"/></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#2124.62.28:2140.62.44"/></metadata>
......@@ -418,7 +418,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2159.63.2:2216.63.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/arithmetic_rules.mmt#2173.63.16:2201.63.44"/></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/arithmetic_rules.mmt#2174.63.17:2174.63.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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/arithmetic_rules.mmt#2176.63.19:2176.63.19"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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/arithmetic_rules.mmt#2178.63.21:2178.63.21"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></om:OMS></type></om:OMV></om:OMBVAR>
<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/arithmetic_rules.mmt#2174.63.17:2174.63.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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/arithmetic_rules.mmt#2176.63.19:2176.63.19"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Numbers" name="tmrat"></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/arithmetic_rules.mmt#2178.63.21:2178.63.21"/></metadata><type><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#713.23.13:713.23.13"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2181.63.24:2201.63.44"/></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#2185.63.28:2201.63.44"/></metadata>
......
......@@ -6,7 +6,7 @@
</constant><constant name="tmnat">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2883.81.2:2914.81.33"/></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/arithmetic_rules.mmt#2891.81.10:2894.81.13"/></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/arithmetic_rules.mmt#2985.84.13:2985.84.13"/></metadata>
<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/arithmetic_rules.mmt#2900.81.19:2905.81.24"/></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="tm"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2900.81.19:2901.81.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="nat"></om:OMS>
</om:OMA></om:OMOBJ></definition>
......@@ -25,7 +25,7 @@
<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>
<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"></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#2994.84.22:2994.84.22"/></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#2990.84.18:2990.84.18"/></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#2994.84.22:2994.84.22"/></metadata></om:OMS>
</om:OMA><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#2999.84.27:2999.84.27"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
......@@ -48,7 +48,17 @@
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><om:OMV name="n"><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/arithmetic_rules.mmt#3094.87.26:3094.87.26"/></metadata><type><om:OMA>
<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="tm"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="m"><type><om:OMA>
<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="tm"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="nat"></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="nat"></om:OMS>
</om:OMBIND>
<om:OMV name="m"></om:OMV>
</om:OMA>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3097.87.29:3142.87.74"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
......@@ -56,7 +66,7 @@
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="sum"></om:OMS><om:OMV name="m"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3099.87.31:3099.87.31"/></metadata></om:OMV><om:OMV name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3104.87.36:3104.87.36"/></metadata></om:OMV><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3106.87.38:3112.87.44"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></om:OMS>
<om:OMBVAR><om:OMV name="i"><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/arithmetic_rules.mmt#3108.87.40:3108.87.40"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="tmnat"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMBVAR><om:OMV name="i"><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/arithmetic_rules.mmt#3108.87.40:3108.87.40"/></metadata><type><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#2990.84.18:2990.84.18"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3110.87.42:3111.87.43"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Sums" name="incl"></om:OMS><om:OMV name="i"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#3111.87.43:3111.87.43"/></metadata></om:OMV>
......
......@@ -17,7 +17,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1445.55.2:1469.55.26"/></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/programming/rabe_encodings.mmt#1450.55.7:1468.55.25"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Machine" name="obj"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1450.55.7:1452.55.9"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Machine" name="loc"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Machine" name="command"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1462.55.19:1468.55.25"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Machine" name="obj"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1450.55.7:1452.55.9"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Machine" name="loc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1456.55.13:1458.55.15"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Machine" name="command"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1462.55.19:1468.55.25"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
......
......@@ -54,7 +54,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#235.13.2:250.13.17"/></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/programming/syntax.mmt#242.13.9:249.13.16"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#242.13.9:245.13.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Nat"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#242.13.9:245.13.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#247.13.14:249.13.16"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
......@@ -206,7 +206,7 @@
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#737.24.10:740.24.13"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#742.24.15:745.24.18"/></metadata></om:OMS>
</om:OMA><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#749.24.22:757.24.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#749.24.22:752.24.25"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#749.24.22:752.24.25"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#754.24.27:757.24.30"/></metadata></om:OMS>
</om:OMA><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#761.24.34:769.24.42"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#761.24.34:764.24.37"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#766.24.39:769.24.42"/></metadata></om:OMS>
......@@ -217,13 +217,13 @@
<om:OMBVAR><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/programming/syntax.mmt#783.25.11:783.25.11"/></metadata><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#742.24.15:745.24.18"/></metadata></om:OMS>
</om:OMA></type></om:OMV><om:OMV name="c"><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/programming/syntax.mmt#785.25.13:785.25.13"/></metadata><type><om:OMA>
</om:OMA></type></om:OMV><om:OMV name="c"><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/programming/syntax.mmt#785.25.13:785.25.13"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#749.24.22:757.24.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#754.24.27:757.24.30"/></metadata></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#788.25.16:808.25.36"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="ifte"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"></om:OMS><om:OMV name="b"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#791.25.19:791.25.19"/></metadata></om:OMV><om:OMV name="c"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#798.25.26:798.25.26"/></metadata></om:OMV><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#805.25.33:808.25.36"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="ifte"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#754.24.27:757.24.30"/></metadata></om:OMS><om:OMV name="b"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#791.25.19:791.25.19"/></metadata></om:OMV><om:OMV name="c"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#798.25.26:798.25.26"/></metadata></om:OMV><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#805.25.33:808.25.36"/></metadata></om:OMS>
</om:OMA>
</om:OMBIND></om:OMOBJ></definition>
......@@ -369,7 +369,7 @@
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1139.36.23:1142.36.26"/></metadata></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1144.36.28:1144.36.28"/></metadata></om:OMV>
</om:OMA><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1148.36.32:1156.36.40"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1148.36.32:1151.36.35"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="prog"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1148.36.32:1151.36.35"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/programs" module="Syntax" name="Unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1153.36.37:1156.36.40"/></metadata></om:OMS>
</om:OMA>
</om:OMA>
</om:OMBIND></om:OMOBJ></type>
......
<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
<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#2569.67.0:2639.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#2602.68.1:2615.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#2620.69.1:2635.69.16"/></metadata></import></theory></omdoc>
\ No newline at end of file
......@@ -26,7 +26,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1739.38.2:1784.38.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/tutorial/1-sfol.mmt#1747.38.10:1764.38.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1761.38.24:1764.38.27"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1754.38.17:1757.38.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1761.38.24:1764.38.27"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="15" fixity="mixfix" arguments="1 ∧ 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -34,7 +34,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1788.39.2:1833.39.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/tutorial/1-sfol.mmt#1796.39.10:1813.39.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1810.39.24:1813.39.27"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1803.39.17:1806.39.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1810.39.24:1813.39.27"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="15" fixity="mixfix" arguments="1 ∨ 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -42,7 +42,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1837.40.2:1882.40.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/tutorial/1-sfol.mmt#1845.40.10:1862.40.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1859.40.24:1862.40.27"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1852.40.17:1855.40.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#1859.40.24:1862.40.27"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="10" fixity="mixfix" arguments="1 ⇒ 2"> <scope languages="" priority="0"/> </notation></notations>
......@@ -64,11 +64,11 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#2786.55.2:2866.56.33"/></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/tutorial/1-sfol.mmt#2794.55.10:2811.55.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#2808.55.24:2811.55.27"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#2801.55.17:2804.55.20"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#2808.55.24:2811.55.27"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND>
<definition><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/tutorial/1-sfol.mmt#2843.56.10:2865.56.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="lambda"></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/tutorial/1-sfol.mmt#2844.56.11:2844.56.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></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/tutorial/1-sfol.mmt#2846.56.13:2846.56.13"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></om:OMS></type></om:OMV></om:OMBVAR>
<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/tutorial/1-sfol.mmt#2844.56.11:2844.56.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"></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/tutorial/1-sfol.mmt#2846.56.13:2846.56.13"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#2801.55.17:2804.55.20"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#2849.56.16:2865.56.32"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="and"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#2849.56.16:2855.56.22"/></metadata>
......
......@@ -2,7 +2,7 @@
<metadata><meta property="http://purl.org/dc/terms?_?description"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMSF><om:text format=""><![CDATA[the unit element of the monoid]]></om:text></om:OMSF></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#869.22.1:934.22.66"/></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/tutorial/2-algebra.mmt#876.22.8:879.22.11"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#879.22.11:879.22.11"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="e"> <scope languages="" priority="0"/> </notation></notations>
......@@ -20,7 +20,7 @@
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1044.25.21:1052.25.29"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="equal"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1044.25.21:1048.25.25"/></metadata>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="equal"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#265.7.27:265.7.27"/></metadata></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1044.25.21:1048.25.25"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="comp"></om:OMS><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1044.25.21:1044.25.21"/></metadata></om:OMV><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Monoid" name="unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1048.25.25:1048.25.25"/></metadata></om:OMS>
</om:OMA><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1052.25.29:1052.25.29"/></metadata></om:OMV>
......
......@@ -7,7 +7,7 @@
</constant><constant name="ℕ">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/3-literalsrules.mmt#320.8.1:331.8.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/tutorial/1-sfol.mmt#3291.65.18:3294.65.21"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<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/tutorial/3-literalsrules.mmt#324.8.5:329.8.10"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Nat" name="Nat"></om:OMS>
</om:OMA></om:OMOBJ></definition>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="DerivedUnits" base="http://cds.omdoc.org/physics" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3370.95.0:3581.101.0"/></metadata><import from="http://cds.omdoc.org/physics?Prefixes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3404.96.3:3421.96.20"/></metadata></import><import from="http://cds.omdoc.org/physics?Units"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3426.97.3:3440.97.17"/></metadata></import><constant name="litre">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3449.99.3:3532.99.86"/></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/quantities.mmt#3458.99.12:3465.99.19"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="DerivedUnits" base="http://cds.omdoc.org/physics" meta="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3366.95.0:3577.101.0"/></metadata><import from="http://cds.omdoc.org/physics?Prefixes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3400.96.3:3417.96.20"/></metadata></import><import from="http://cds.omdoc.org/physics?Units"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3422.97.3:3436.97.17"/></metadata></import><constant name="litre">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3445.99.3:3528.99.86"/></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/quantities.mmt#3454.99.12:3461.99.19"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/physics" module="Quantities" name="quantity"></om:OMS><om:OMS base="http://cds.omdoc.org/physics" module="Dimensions" name="volume"></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant><constant name="litres">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3537.100.3:3579.100.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/quantities.mmt#3546.100.12:3556.100.22"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3533.100.3:3575.100.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/quantities.mmt#3542.100.12:3552.100.22"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/physics" module="Quantities" name="unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3546.100.12:3549.100.15"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/physics" module="Dimensions" name="volume"></om:OMS>
<om:OMS base="http://cds.omdoc.org/physics" module="Quantities" name="unit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3542.100.12:3545.100.15"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/physics" module="Dimensions" name="volume"></om:OMS>
</om:OMA></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/quantities.mmt#3561.100.27:3578.100.44"/></metadata>
<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/quantities.mmt#3557.100.27:3574.100.44"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/physics" module="Quantities" name="multiples_of"></om:OMS><om:OMS base="http://cds.omdoc.org/physics" module="Dimensions" name="volume"></om:OMS><om:OMS base="http://cds.omdoc.org/physics" module="DerivedUnits" name="litre"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3574.100.40:3578.100.44"/></metadata></om:OMS>
<om:OMS base="http://cds.omdoc.org/physics" module="Quantities" name="multiples_of"></om:OMS><om:OMS base="http://cds.omdoc.org/physics" module="Dimensions" name="volume"></om:OMS><om:OMS base="http://cds.omdoc.org/physics" module="DerivedUnits" name="litre"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3570.100.40:3574.100.44"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file