Commit 88723973 authored by Florian Rabe's avatar Florian Rabe

no message

parent 90aeafe4
<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:143.6.1"/></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:108.3.15"/></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:124.4.15"/></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:141.5.16"/></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="Counter" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#388.15.0:485.18.1"/></metadata><constant name="counter">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#419.16.2:436.16.19"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Counter" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#388.15.0:484.18.0"/></metadata><constant name="counter">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#419.16.2:435.16.18"/></metadata>
<type><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/program.mmt#428.16.11:430.16.13"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="0"/></om:OMOBJ></definition>
</constant><constant name="add">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#439.17.2:483.17.46"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#439.17.2:482.17.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/program.mmt#444.17.7:453.17.16"/></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/urtheories" module="CF" name="None"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#450.17.13:453.17.16"/></metadata></om:OMS>
......
<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#642.21.0:758.24.1"/></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#696.22.2:709.22.15"/></metadata></import><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#712.23.2:756.23.46"/></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#721.23.11:738.23.28"/></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#735.23.25:738.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"></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>
......
<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:638.19.1"/></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:390.12.15"/></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:411.13.20"/></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:454.14.40"/></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:512.15.57"/></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:574.17.60"/></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:636.18.61"/></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><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#42.2.0:152.8.1"/></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:88.3.15"/></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:146.6.21"/></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><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#501.28.0:755.33.1"/></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:578.29.21"/></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><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#135.4.0:317.9.1"/></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:199.5.14"/></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:215.6.15"/></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:265.7.49"/></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:315.8.49"/></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>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FlexaryQuantifiers" 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/sequences.mmt#639.19.0:1090.29.1"/></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/sequences.mmt#679.20.2:692.20.15"/></metadata></import><constant name="flexforall">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#696.22.2:743.22.49"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FlexaryQuantifiers" 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/sequences.mmt#639.19.0:1089.29.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/sequences.mmt#679.20.2:691.20.14"/></metadata></import><constant name="flexforall">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#696.22.2:742.22.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/sequences.mmt#709.22.15:734.22.40"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></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/sequences.mmt#710.22.16:710.22.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -17,7 +17,7 @@
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="∀* 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="flexforallI">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#746.23.2:815.23.71"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#746.23.2:814.23.70"/></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/sequences.mmt#759.23.15:813.23.69"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></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/sequences.mmt#760.23.16:760.23.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"></om:OMS></type></om:OMV><om:OMV name="F"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#763.23.19:763.23.19"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#766.23.22:778.23.34"/></metadata>
......@@ -65,7 +65,7 @@
<notations></notations>
</constant><constant name="flexforallE">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#818.24.2:887.24.71"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#818.24.2:886.24.70"/></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/sequences.mmt#831.24.15:885.24.69"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></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/sequences.mmt#832.24.16:832.24.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"></om:OMS></type></om:OMV><om:OMV name="F"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#835.24.19:835.24.19"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#838.24.22:850.24.34"/></metadata>
......@@ -113,7 +113,7 @@
<notations></notations>
</constant><constant name="flexexists">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#891.26.2:938.26.49"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#891.26.2:937.26.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/sequences.mmt#904.26.15:929.26.40"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></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/sequences.mmt#905.26.16:905.26.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -131,7 +131,7 @@
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="∃* 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="flexexistsI">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#941.27.2:1008.27.69"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#941.27.2:1007.27.68"/></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/sequences.mmt#954.27.15:1006.27.67"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></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/sequences.mmt#955.27.16:955.27.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"></om:OMS></type></om:OMV><om:OMV name="F"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#958.27.19:958.27.19"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#961.27.22:973.27.34"/></metadata>
......@@ -179,7 +179,7 @@
<notations></notations>
</constant><constant name="flexexistsE">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#1011.28.2:1088.28.79"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#1011.28.2:1087.28.78"/></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/sequences.mmt#1024.28.15:1086.28.77"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></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/sequences.mmt#1025.28.16:1025.28.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"></om:OMS></type></om:OMV><om:OMV name="F"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#1028.28.19:1028.28.19"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#1031.28.22:1043.28.34"/></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><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#315.13.0:582.18.1"/></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:393.14.20"/></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:519.15.21"/></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:548.16.28"/></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:580.17.31"/></metadata>
<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>
<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/literals.mmt#561.17.12:568.17.19"/></metadata>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="IntRules" 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#270.10.0:681.20.1"/></metadata><import from="http://cds.omdoc.org/examples?Int"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#327.11.2:340.11.15"/></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/int.mmt#344.12.2:362.12.20"/></metadata></import><constant name="times_mono">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#366.14.2:438.14.74"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="IntRules" 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#270.10.0:680.20.0"/></metadata><import from="http://cds.omdoc.org/examples?Int"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#327.11.2:338.11.13"/></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/int.mmt#344.12.2:361.12.19"/></metadata></import><constant name="times_mono">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#366.14.2:437.14.73"/></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#382.14.18:436.14.72"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="X"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#383.14.19:383.14.19"/></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/int.mmt#385.14.21:387.14.23"/></metadata></om:OMS></type></om:OMV><om:OMV name="Y"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#389.14.25:389.14.25"/></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/int.mmt#391.14.27:393.14.29"/></metadata></om:OMS></type></om:OMV><om:OMV name="Z"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#395.14.31:395.14.31"/></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/int.mmt#397.14.33:399.14.35"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -35,7 +35,7 @@
<notations></notations>
</constant><constant name="times_invmono">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#441.15.2:503.15.64"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#441.15.2:502.15.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/int.mmt#457.15.18:499.15.60"/></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#458.15.19:458.15.19"/></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#460.15.21:460.15.21"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></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/int.mmt#462.15.23:462.15.23"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -71,7 +71,7 @@
<notations></notations>
</constant><constant name="succ_invert" role="Simplify">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#509.17.2:561.17.54"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#509.17.2:560.17.53"/></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#526.17.19:544.17.37"/></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#527.17.20:527.17.20"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -92,7 +92,7 @@
<notations></notations>
</constant><constant name="plus_invert_R" role="Simplify">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#564.18.2:620.18.58"/></metadata>
<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>
......@@ -113,7 +113,7 @@
<notations></notations>
</constant><constant name="plus_invert_L" role="Simplify">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#623.19.2:679.19.58"/></metadata>
<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>
......
<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:268.8.1"/></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:107.3.15"/></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:130.4.22"/></metadata>
<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:176.5.45"/></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:220.6.43"/></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:266.7.45"/></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="Lists" 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#586.16.1:946.25.1"/></metadata><import from="http://cds.omdoc.org/examples?Equality"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#641.17.2:659.17.20"/></metadata></import><constant name="list">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#662.18.2:682.18.22"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Lists" 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#586.16.1:945.25.0"/></metadata><import from="http://cds.omdoc.org/examples?Equality"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#641.17.2:658.17.19"/></metadata></import><constant name="list">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#662.18.2:681.18.21"/></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/shallow_polymorphism.mmt#670.18.10:680.18.20"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></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/shallow_polymorphism.mmt#677.18.17:680.18.20"/></metadata></om:OMS>
......@@ -7,7 +7,7 @@
</constant><constant name="nil">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#685.19.2:715.19.32"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#685.19.2:714.19.31"/></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#693.19.10:702.19.19"/></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#694.19.11:694.19.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -19,7 +19,7 @@
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="nil %I1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="cons">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#718.20.2:767.20.51"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#718.20.2:766.20.50"/></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#726.20.10:748.20.32"/></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#727.20.11:727.20.11"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -37,7 +37,7 @@
<notations><notation dimension="1" precedence="75" fixity="mixfix" arguments="2 , 3"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="append">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#771.22.2:826.22.57"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#771.22.2:825.22.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/shallow_polymorphism.mmt#780.22.11:807.22.38"/></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#781.22.12:781.22.12"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV></om:OMBVAR>
......@@ -58,7 +58,7 @@
<notations><notation dimension="1" precedence="75" fixity="mixfix" arguments="2 + 3"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="append_nil">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#829.23.2:870.23.43"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#829.23.2:869.23.42"/></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#843.23.16:868.23.41"/></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#844.23.17:844.23.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV><om:OMV name="m"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#847.23.20:847.23.20"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#850.23.23:855.23.28"/></metadata>
......@@ -82,7 +82,7 @@
</constant><constant name="append_cons">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#873.24.2:944.24.73"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#873.24.2:943.24.72"/></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#887.24.16:942.24.71"/></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#888.24.17:888.24.17"/></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#891.24.20:891.24.20"/></metadata><type><om:OMV name="a"></om:OMV></type></om:OMV><om:OMV name="l"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#897.24.26:897.24.26"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#900.24.29:905.24.34"/></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:287.12.1"/></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:213.9.16"/></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:267.10.53"/></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:285.11.17"/></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="Monoid" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?FOLPatterns"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#154.10.0:202.12.1"/></metadata><derived feature="instance" name="comp" base="http://cds.omdoc.org/examples"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#191.11.6:199.11.14"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Monoid" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?FOLPatterns"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#154.10.0:201.12.0"/></metadata><derived feature="instance" name="comp" base="http://cds.omdoc.org/examples"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#191.11.6:199.11.14"/></metadata>
<om:OMS base="http://cds.omdoc.org/examples" module="FOLPatterns/fun"></om:OMS>
<om:OMLIT type="http://cds.omdoc.org/urtheories?NatSymbols?NAT" value="2"/>
</om:OMA></type></derived></theory></omdoc>
\ No newline at end of file
<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:311.11.1"/></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:158.5.20"/></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:180.6.21"/></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:209.7.28"/></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:309.10.29"/></metadata>
<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>
<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/literals.mmt#292.10.12:298.10.18"/></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="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:499.26.1"/></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:368.20.20"/></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:406.22.34"/></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><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#191.6.0:386.13.1"/></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:267.7.21"/></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:288.8.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/program.mmt#291.9.2:317.9.28"/></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:361.11.40"/></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>
......@@ -10,4 +10,4 @@
</om:OMBIND></om:OMOBJ></type>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="print 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><ruleconstant name="[scala://mmt.kwarc.info/cf?Print]"><type><om:OMS base="scala://mmt.kwarc.info/cf" module="Print"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#369.12.7:382.12.20"/></metadata></om:OMS></type></ruleconstant></theory></omdoc>
\ No newline at end of file
</constant><ruleconstant name="[scala://mmt.kwarc.info/cf?Print]"><type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="scala://mmt.kwarc.info/cf" module="Print"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#369.12.7:382.12.20"/></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="Program" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#491.20.0:660.29.1"/></metadata><constant name="main">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#522.21.2:537.21.17"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Program" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#491.20.0:659.29.0"/></metadata><constant name="main">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#522.21.2:536.21.16"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="CF" name="None"></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/program.mmt#529.21.9:535.21.15"/></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="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:491.15.1"/></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:252.7.13"/></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:299.9.45"/></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:348.10.48"/></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:394.11.45"/></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,14 +28,14 @@
<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:438.12.43"/></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>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="15" fixity="mixfix" arguments="1 / 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><ruleconstant name="[scala://lf.mmt.kwarc.info/?Realize]/2019407922"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#449.14.7:487.14.45"/></metadata>
</constant><ruleconstant name="[scala://lf.mmt.kwarc.info/?Realize]/2019407922"><type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="scala://lf.mmt.kwarc.info/" module="Realize"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#449.14.7:463.14.21"/></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#465.14.23:468.14.26"/></metadata></om:OMS><om:OMS base="scala://uom.api.mmt.kwarc.info/" module="StandardRat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#470.14.28:487.14.45"/></metadata></om:OMS>
</om:OMA></type></ruleconstant></theory></omdoc>
\ No newline at end of file
</om:OMA></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="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:3147.88.1"/></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:2861.78.19"/></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:2880.80.17"/></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>
</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:2915.81.34"/></metadata>
<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>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
......@@ -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:2970.82.54"/></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:3067.86.32"/></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:3145.87.77"/></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="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:445.17.1"/></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:406.15.13"/></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:443.16.36"/></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>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="DHOL" 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#447.19.0:601.24.1"/></metadata><import from="http://cds.omdoc.org/examples/ijcar?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#483.20.2:496.20.15"/></metadata></import><import from="http://cds.omdoc.org/examples/ijcar?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#499.21.2:513.21.16"/></metadata></import><ruleconstant name="[scala://mmt.kwarc.info/lf?ShallowPolymorphism]"><type><om:OMS base="scala://mmt.kwarc.info/lf" module="ShallowPolymorphism"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#521.22.7:548.22.34"/></metadata></om:OMS></type></ruleconstant><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#553.23.2:599.23.48"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="DHOL" 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#447.19.0:600.24.0"/></metadata><import from="http://cds.omdoc.org/examples/ijcar?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#483.20.2:495.20.14"/></metadata></import><import from="http://cds.omdoc.org/examples/ijcar?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#499.21.2:512.21.15"/></metadata></import><ruleconstant name="[scala://mmt.kwarc.info/lf?ShallowPolymorphism]"><type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="scala://mmt.kwarc.info/lf" module="ShallowPolymorphism"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#521.22.7:548.22.34"/></metadata></om:OMS></om:OMOBJ></type></ruleconstant><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#553.23.2:598.23.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/IJCAR2018_example.mmt#561.23.10:581.23.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/IJCAR2018_example.mmt#562.23.11:562.23.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/IJCAR2018_example.mmt#564.23.13:567.23.16"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Double" base="http://cds.omdoc.org/examples/ijcar" meta="http://cds.omdoc.org/examples/ijcar?DHOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#603.26.0:729.30.1"/></metadata><constant name="double">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#629.27.2:648.27.21"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Double" base="http://cds.omdoc.org/examples/ijcar" meta="http://cds.omdoc.org/examples/ijcar?DHOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#603.26.0:728.30.0"/></metadata><constant name="double">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#629.27.2:647.27.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/IJCAR2018_example.mmt#638.27.11:646.27.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="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#638.27.11:640.27.13"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples/ijcar" module="Nat" name="nat"></om:OMS>
......@@ -7,7 +7,7 @@
</constant><constant name="double_zero">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#651.28.2:679.28.30"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#651.28.2:678.28.29"/></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#664.28.15:677.28.28"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/ijcar" module="Bool" name="proof"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#666.28.17:677.28.28"/></metadata>
......@@ -21,7 +21,7 @@
</constant><constant name="double_succ">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#682.29.2:727.29.47"/></metadata>
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#682.29.2:726.29.46"/></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/IJCAR2018_example.mmt#695.29.15:725.29.45"/></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/IJCAR2018_example.mmt#696.29.16:696.29.16"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples/ijcar" module="Nat" name="nat"></om:OMS></type></om:OMV></om:OMBVAR>
......
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Nat" 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#87.4.0:358.12.1"/></metadata><constant name="nat">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#121.5.2:132.5.13"/></metadata>
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Nat" 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#87.4.0:357.12.0"/></metadata><constant name="nat">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#121.5.2:131.5.12"/></metadata>