Commit 85f0bc9b authored by Florian Rabe's avatar Florian Rabe

no message

Merge branch 'devel' of gl.mathhub.info:MMT/examples into devel

# Conflicts:
#	content/http..cds.omdoc.org/ignore/$Null$Pointer$Bug$Example.omdoc.xz
parents 358543e8 19dc06e5
......@@ -3,7 +3,7 @@ narration-base: http://docs.omdoc.org/examples
ns : http://cds.omdoc.org/examples
dependencies: MMT/urtheories
classpath: bin
scala: scala_realizations export/scala export/lf-scala
scala: scala scala_realizations export/scala export/lf-scala
responsible: florian.rabe@kwarc.info
title: MMT examples
teaser: various examples for MMT's native source syntax
......
<errors>
<error type="info.kwarc.mmt.api.checking.MMTStructureChecker$$anon$1" shortMsg="invalid element: View is not total: http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?ListMonad" level="1">
http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad?neutral_left
http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad?neutral_right
http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad?assoc
<stacktrace>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkElementEnd(MMTStructureChecker.scala:413)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementEnd(MMTStructureChecker.scala:80)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElementEnd(Interpreter.scala:90)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.end(StructureParser.scala:113)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readView(StructureParser.scala:761)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:411)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:133)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</errors>
<errors>
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: http://cds.omdoc.org/examples?LeftRegular12Normal?[http://cds.omdoc.org/examples?LeftRegular1]/leftregular1?definition: Judgment |- [x,y,z]trans3 sym idempotent (/_/3 x y z) idempotent : {x,y,z}⊦((z∘x)∘z)∘y≐(z∘x)∘y" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:91)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15$adapted(RuleBasedChecker.scala:90)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$13(RuleBasedChecker.scala:90)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:87)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16(MMTStructureChecker.scala:301)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16$adapted(MMTStructureChecker.scala:277)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:277)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readView$1(StructureParser.scala:759)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readView(StructureParser.scala:759)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:415)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:133)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: http://cds.omdoc.org/examples?RightRegular12Normal?[http://cds.omdoc.org/examples?RightRegular1]/rightregular1?definition: Judgment |- [x,y,z]trans3 sym idempotent (/_/3 x y z) idempotent : {x,y,z}⊦((x∘z)∘y)∘z≐(x∘y)∘z" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:91)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15$adapted(RuleBasedChecker.scala:90)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$13(RuleBasedChecker.scala:90)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:87)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16(MMTStructureChecker.scala:301)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16$adapted(MMTStructureChecker.scala:277)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:277)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readView$1(StructureParser.scala:759)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readView(StructureParser.scala:759)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:415)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:133)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</errors>
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#0.0.0:2375.85.0"/></metadata><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Types]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Types"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#79.2.0:90.2.11"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Logic]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Logic"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#153.7.0:164.7.11"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Equality]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Equality"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#243.12.0:257.12.14"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?STT]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?STT"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#535.22.0:544.22.9"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Eta]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Eta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#782.32.0:791.32.9"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Extensionality]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Extensionality"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#880.37.0:900.37.20"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?List]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?List"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#1111.47.0:1121.47.10"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#1716.61.0:1727.61.11"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?ListMonad]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?ListMonad"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#2112.71.0:2125.71.13"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#2307.81.0:2322.81.15"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/IFIP21_tutorial.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#0.0.0:2373.84.0"/></metadata><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Types]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Types"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#79.2.0:90.2.11"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Logic]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Logic"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#153.7.0:164.7.11"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Equality]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Equality"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#243.12.0:257.12.14"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?STT]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?STT"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#535.22.0:544.22.9"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Eta]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Eta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#782.32.0:791.32.9"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Extensionality]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Extensionality"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#880.37.0:900.37.20"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?List]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?List"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#1111.47.0:1121.47.10"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#1716.61.0:1727.61.11"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?ListMonad]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?ListMonad"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#2112.71.0:2125.71.13"/></metadata></mref><mref name="[http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus]" target="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?MonadPlus"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#2307.81.0:2322.81.15"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/IJCAR2018_example.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#0.0.0:730.31.0"/></metadata><mref name="[http://cds.omdoc.org/examples/ijcar?Nat]" target="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#87.4.0:96.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/ijcar?Bool]" target="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#360.14.0:370.14.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/ijcar?DHOL]" target="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#447.19.0:457.19.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/ijcar?Double]" target="http://cds.omdoc.org/examples/ijcar?Double"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#603.26.0:615.26.12"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/IJCAR2018_example.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#0.0.0:728.30.0"/></metadata><mref name="[http://cds.omdoc.org/examples/ijcar?Nat]" target="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#87.4.0:96.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/ijcar?Bool]" target="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#360.14.0:370.14.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/ijcar?DHOL]" target="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#447.19.0:457.19.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/ijcar?Double]" target="http://cds.omdoc.org/examples/ijcar?Double"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IJCAR2018_example.mmt#603.26.0:615.26.12"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/argumentation.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/argumentation.mmt#0.0.0:717.25.0"/></metadata><mref name="[http://cds.omdoc.org/examples?TopologicalArgumentationTheory]" target="http://cds.omdoc.org/examples?TopologicalArgumentationTheory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/argumentation.mmt#42.2.0:78.2.36"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/arithmetic_rules.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#0.0.0:3148.89.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Numbers]" target="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#121.4.0:134.4.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Rules]" target="http://cds.omdoc.org/examples?Rules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#960.34.0:971.34.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Sums]" target="http://cds.omdoc.org/examples?Sums"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2791.77.0:2801.77.10"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/arithmetic_rules.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#0.0.0:3146.88.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Numbers]" target="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#121.4.0:134.4.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Rules]" target="http://cds.omdoc.org/examples?Rules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#960.34.0:971.34.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Sums]" target="http://cds.omdoc.org/examples?Sums"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/arithmetic_rules.mmt#2791.77.0:2801.77.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/bands.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#0.0.0:3744.139.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#42.2.0:307.9.0"/></metadata>regular bands and views between them
mostly following the wikipedia page on Bands
Notes:
- some names that were not given on Wikipedia are made up
- most views do not actually use (all of) the Band properties
- LeftX and RightX are stronger than X, not weaker</opaque><mref name="[http://cds.omdoc.org/examples?Regular]" target="http://cds.omdoc.org/examples?Regular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#310.11.0:323.11.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?LeftRegular1]" target="http://cds.omdoc.org/examples?LeftRegular1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#405.16.0:423.16.18"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?LeftRegular]" target="http://cds.omdoc.org/examples?LeftRegular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#506.21.0:523.21.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightRegular1]" target="http://cds.omdoc.org/examples?RightRegular1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#599.26.0:618.26.19"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightRegular]" target="http://cds.omdoc.org/examples?RightRegular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#702.31.0:720.31.18"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#797.36.0:852.36.55"/></metadata>views for the three stages of regular band theories</opaque><mref name="[http://cds.omdoc.org/examples?Regular2LeftRegular1]" target="http://cds.omdoc.org/examples?Regular2LeftRegular1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#855.38.0:888.38.33"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?LeftRegular12LeftRegular]" target="http://cds.omdoc.org/examples?LeftRegular12LeftRegular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#994.43.0:1031.43.37"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Regular2RightRegular1]" target="http://cds.omdoc.org/examples?Regular2RightRegular1"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1145.48.0:1179.48.34"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightRegular12RightRegular]" target="http://cds.omdoc.org/examples?RightRegular12RightRegular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1334.53.0:1373.53.39"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1530.58.0:1546.58.16"/></metadata>normal bands</opaque><mref name="[http://cds.omdoc.org/examples?Normal]" target="http://cds.omdoc.org/examples?Normal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1549.60.0:1561.60.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?LeftNormal]" target="http://cds.omdoc.org/examples?LeftNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1644.65.0:1660.65.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightNormal]" target="http://cds.omdoc.org/examples?RightNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1743.70.0:1760.70.17"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1844.75.0:1927.75.83"/></metadata>views for the diamond of normal band theories (with semilattices at the bottom)</opaque><mref name="[http://cds.omdoc.org/examples?Normal2LeftNormal]" target="http://cds.omdoc.org/examples?Normal2LeftNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#1930.77.0:1960.77.30"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Normal2RightNormal]" target="http://cds.omdoc.org/examples?Normal2RightNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#2060.82.0:2091.82.31"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?LeftNormal2Semilattice]" target="http://cds.omdoc.org/examples?LeftNormal2Semilattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#2215.87.0:2241.87.26"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightNormal2Semilattice]" target="http://cds.omdoc.org/examples?RightNormal2Semilattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#2344.92.0:2380.92.36"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#2485.97.0:2531.97.46"/></metadata>views from regular to normal band theories</opaque><mref name="[http://cds.omdoc.org/examples?LeftRegular12Normal]" target="http://cds.omdoc.org/examples?LeftRegular12Normal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#2534.99.0:2566.99.32"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?LeftRegular2LeftNormal]" target="http://cds.omdoc.org/examples?LeftRegular2LeftNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#2763.105.0:2798.105.35"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightRegular12Normal]" target="http://cds.omdoc.org/examples?RightRegular12Normal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#2939.110.0:2972.110.33"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightRegular2RightNormal]" target="http://cds.omdoc.org/examples?RightRegular2RightNormal"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#3170.116.0:3207.116.37"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#3345.121.0:3409.121.64"/></metadata>rectangular bands (the axioms here already imply idempotency)</opaque><mref name="[http://cds.omdoc.org/examples?Rectangular]" target="http://cds.omdoc.org/examples?Rectangular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#3412.123.0:3429.123.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?LeftSingular]" target="http://cds.omdoc.org/examples?LeftSingular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#3563.131.0:3581.131.18"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?RightSingular]" target="http://cds.omdoc.org/examples?RightSingular"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/bands.mmt#3654.136.0:3673.136.19"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/base-arith.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/base-arith.mmt#0.0.0:1192.32.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Binary]" target="http://cds.omdoc.org/examples?Binary"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/base-arith.mmt#67.3.0:79.3.12"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/equivalence.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/equivalence.mmt#0.0.0:461.19.0"/></metadata><mref name="[http://cds.omdoc.org/examples?LFEq]" target="http://cds.omdoc.org/examples?LFEq"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/equivalence.mmt#138.5.0:148.5.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?trivialEquivExample]" target="http://cds.omdoc.org/examples?trivialEquivExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/equivalence.mmt#210.10.0:235.10.25"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/hott.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/hott.mmt#0.0.0:7781.155.0"/></metadata><mref name="[http://cds.omdoc.org/examples?HOTT]" target="http://cds.omdoc.org/examples?HOTT"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/hott.mmt#427.7.0:437.7.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/inductive.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#0.0.0:780.39.0"/></metadata><mref name="[http://cds.omdoc.org/examples?LFI]" target="http://cds.omdoc.org/examples?LFI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#103.4.0:112.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatExample]" target="http://cds.omdoc.org/examples?NatExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#169.9.0:185.9.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?TestExample]" target="http://cds.omdoc.org/examples?TestExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#260.17.0:277.17.17"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/inductive.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#0.0.0:778.38.0"/></metadata><mref name="[http://cds.omdoc.org/examples?LFI]" target="http://cds.omdoc.org/examples?LFI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#103.4.0:112.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatExample]" target="http://cds.omdoc.org/examples?NatExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#169.9.0:185.9.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?TestExample]" target="http://cds.omdoc.org/examples?TestExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#260.17.0:277.17.17"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/instances.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/instances.mmt#0.0.0:724.35.0"/></metadata></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/instances.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/instances.mmt#0.0.0:722.34.0"/></metadata></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/int.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#0.0.0:680.20.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Int]" target="http://cds.omdoc.org/examples?Int"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#42.2.0:51.2.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?IntRules]" target="http://cds.omdoc.org/examples?IntRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#270.10.0:284.10.14"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/literals.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#0.0.0:1692.49.0"/></metadata><mref name="[http://cds.omdoc.org/examples?NatLiterals]" target="http://cds.omdoc.org/examples?NatLiterals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#80.4.0:97.4.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?IntLiterals]" target="http://cds.omdoc.org/examples?IntLiterals"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#315.13.0:332.13.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Vectors]" target="http://cds.omdoc.org/examples?Vectors"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#584.20.0:597.20.13"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/fol.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#0.0.0:1372.39.0"/></metadata><mref name="[http://cds.omdoc.org/examples?FOL]" target="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#135.4.0:144.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLNatDed]" target="http://cds.omdoc.org/examples?FOLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#319.11.0:334.11.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLEQ]" target="http://cds.omdoc.org/examples?FOLEQ"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#640.21.0:651.21.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLEQNatDed]" target="http://cds.omdoc.org/examples?FOLEQNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#758.26.0:775.26.17"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/linear.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#0.0.0:5195.158.0"/></metadata><mref name="[http://cds.omdoc.org/examples/linear?Syntax]" target="http://cds.omdoc.org/examples/linear?Syntax"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#327.10.0:339.10.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Worlds]" target="http://cds.omdoc.org/examples/linear?Worlds"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#664.25.0:676.25.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Exchange]" target="http://cds.omdoc.org/examples/linear?Exchange"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1331.46.0:1345.46.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Contraction]" target="http://cds.omdoc.org/examples/linear?Contraction"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1581.57.0:1598.57.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?Weakening]" target="http://cds.omdoc.org/examples/linear?Weakening"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#1708.63.0:1723.63.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/linear?ResourceSemantics]" target="http://cds.omdoc.org/examples/linear?ResourceSemantics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/linear.mmt#2124.74.0:2147.74.23"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/pl.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#0.0.0:2889.85.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#42.2.0:137.3.89"/></metadata>Intuitionistic propositional logic with natural deduction rules and a few example proofs</opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#140.5.0:195.6.48"/></metadata>We start with the syntax of propositional logic.</opaque><mref name="[http://cds.omdoc.org/examples?PL]" target="http://cds.omdoc.org/examples?PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#198.8.0:206.8.8"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1233.38.0:1271.38.38"/></metadata>Now we describe the proof theory.</opaque><mref name="[http://cds.omdoc.org/examples?PLNatDed]" target="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/pl.mmt#1282.40.0:1296.40.14"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/logic/prover.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#0.0.0:756.34.0"/></metadata><mref name="[http://cds.omdoc.org/examples?ProverTest]" target="http://cds.omdoc.org/examples?ProverTest"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#42.2.0:58.2.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?PLProofs]" target="http://cds.omdoc.org/examples?PLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#293.19.0:307.19.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLProofs]" target="http://cds.omdoc.org/examples?FOLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#501.28.0:516.28.15"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/logic/prover.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#0.0.0:754.33.0"/></metadata><mref name="[http://cds.omdoc.org/examples?ProverTest]" target="http://cds.omdoc.org/examples?ProverTest"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#42.2.0:58.2.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?PLProofs]" target="http://cds.omdoc.org/examples?PLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#293.19.0:307.19.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FOLProofs]" target="http://cds.omdoc.org/examples?FOLProofs"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#501.28.0:516.28.15"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/magmas.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#0.0.0:1209.52.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Magma]" target="http://cds.omdoc.org/examples?Magma"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#42.2.0:53.2.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Semigroup]" target="http://cds.omdoc.org/examples?Semigroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#119.6.0:134.6.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Commutative]" target="http://cds.omdoc.org/examples?Commutative"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#686.22.0:703.22.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Neutral]" target="http://cds.omdoc.org/examples?Neutral"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#770.27.0:783.27.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Idempotent]" target="http://cds.omdoc.org/examples?Idempotent"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#894.34.0:910.34.16"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Monoid]" target="http://cds.omdoc.org/examples?Monoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#979.39.0:991.39.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Band]" target="http://cds.omdoc.org/examples?Band"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#1055.44.0:1065.44.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Semilattice]" target="http://cds.omdoc.org/examples?Semilattice"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/magmas.mmt#1132.49.0:1149.49.17"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/module_expressions.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#0.0.0:917.23.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Algebra]" target="http://cds.omdoc.org/examples?Algebra"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/module_expressions.mmt#43.2.0:56.2.13"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/nat.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#0.0.0:3591.97.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Bool]" target="http://cds.omdoc.org/examples?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#42.2.0:52.2.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Logic]" target="http://cds.omdoc.org/examples?Logic"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#145.8.0:156.8.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Nat]" target="http://cds.omdoc.org/examples?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#291.14.0:300.14.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatRules]" target="http://cds.omdoc.org/examples?NatRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#709.28.0:723.28.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?NatMinus]" target="http://cds.omdoc.org/examples?NatMinus"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#2609.78.0:2623.78.14"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/patterns.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#0.0.0:203.13.0"/></metadata><mref name="[http://cds.omdoc.org/examples?FOLPatterns]" target="http://cds.omdoc.org/examples?FOLPatterns"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#42.2.0:59.2.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Monoid]" target="http://cds.omdoc.org/examples?Monoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#154.10.0:166.10.12"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/patterns.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#0.0.0:201.12.0"/></metadata><mref name="[http://cds.omdoc.org/examples?FOLPatterns]" target="http://cds.omdoc.org/examples?FOLPatterns"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#42.2.0:59.2.17"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Monoid]" target="http://cds.omdoc.org/examples?Monoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#154.10.0:166.10.12"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/program.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#0.0.0:661.30.0"/></metadata><mref name="[http://cds.omdoc.org/examples?ProgLang]" target="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#191.6.0:205.6.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Counter]" target="http://cds.omdoc.org/examples?Counter"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#388.15.0:401.15.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Program]" target="http://cds.omdoc.org/examples?Program"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#491.20.0:504.20.13"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/program.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#0.0.0:659.29.0"/></metadata><mref name="[http://cds.omdoc.org/examples?ProgLang]" target="http://cds.omdoc.org/examples?ProgLang"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#191.6.0:205.6.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Counter]" target="http://cds.omdoc.org/examples?Counter"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#388.15.0:401.15.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Program]" target="http://cds.omdoc.org/examples?Program"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/program.mmt#491.20.0:504.20.13"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/programming/machine.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/machine.mmt#0.0.0:428.22.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?Machine]" target="http://cds.omdoc.org/examples/programs?Machine"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/machine.mmt#89.4.0:102.4.13"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/programming/machine.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/machine.mmt#0.0.0:426.21.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?Machine]" target="http://cds.omdoc.org/examples/programs?Machine"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/machine.mmt#89.4.0:102.4.13"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/programming/rabe_encodings.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#0.0.0:2981.104.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?Syntax]" target="http://cds.omdoc.org/examples/programs?Syntax"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#51.2.0:63.2.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?Test]" target="http://cds.omdoc.org/examples/programs?Test"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1181.39.0:1191.39.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?Machine]" target="http://cds.omdoc.org/examples/programs?Machine"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1342.49.0:1355.49.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?OperationalSemantics]" target="http://cds.omdoc.org/examples/programs?OperationalSemantics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/rabe_encodings.mmt#1682.68.0:1708.68.26"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/programming/semantics.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/semantics.mmt#0.0.0:1350.38.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?OperationalSemantics]" target="http://cds.omdoc.org/examples/programs?OperationalSemantics"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/semantics.mmt#51.2.0:77.2.26"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/programming/syntax.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#0.0.0:1341.48.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?Syntax]" target="http://cds.omdoc.org/examples/programs?Syntax"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#51.2.0:63.2.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?Test]" target="http://cds.omdoc.org/examples/programs?Test"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1181.39.0:1191.39.10"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/programming/syntax.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#0.0.0:1338.46.0"/></metadata><mref name="[http://cds.omdoc.org/examples/programs?Syntax]" target="http://cds.omdoc.org/examples/programs?Syntax"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#51.2.0:63.2.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/programs?Test]" target="http://cds.omdoc.org/examples/programs?Test"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/programming/syntax.mmt#1181.39.0:1191.39.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/quantities.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#0.0.0:4294.128.0"/></metadata><mref name="[http://cds.omdoc.org/physics?Quantities]" target="http://cds.omdoc.org/physics?Quantities"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#41.2.0:57.2.16"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?Dimensions]" target="http://cds.omdoc.org/physics?Dimensions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#2395.56.0:2411.56.16"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?Prefixes]" target="http://cds.omdoc.org/physics?Prefixes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#2736.72.0:2750.72.14"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?Units]" target="http://cds.omdoc.org/physics?Units"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3021.80.0:3032.80.11"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?DerivedUnits]" target="http://cds.omdoc.org/physics?DerivedUnits"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3366.95.0:3384.95.18"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?CookingUnit]" target="http://cds.omdoc.org/physics?CookingUnit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3580.103.0:3597.103.17"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?TimeUnits]" target="http://cds.omdoc.org/physics?TimeUnits"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3927.116.0:3942.116.15"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?TemperatureUnits]" target="http://cds.omdoc.org/physics?TemperatureUnits"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#4087.122.0:4109.122.22"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/quantities.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#0.0.0:4291.126.0"/></metadata><mref name="[http://cds.omdoc.org/physics?Quantities]" target="http://cds.omdoc.org/physics?Quantities"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#41.2.0:57.2.16"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?Dimensions]" target="http://cds.omdoc.org/physics?Dimensions"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#2395.56.0:2411.56.16"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?Prefixes]" target="http://cds.omdoc.org/physics?Prefixes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#2736.72.0:2750.72.14"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?Units]" target="http://cds.omdoc.org/physics?Units"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3021.80.0:3032.80.11"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?DerivedUnits]" target="http://cds.omdoc.org/physics?DerivedUnits"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3366.95.0:3384.95.18"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?CookingUnit]" target="http://cds.omdoc.org/physics?CookingUnit"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3580.103.0:3597.103.17"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?TimeUnits]" target="http://cds.omdoc.org/physics?TimeUnits"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#3927.116.0:3942.116.15"/></metadata></mref><mref name="[http://cds.omdoc.org/physics?TemperatureUnits]" target="http://cds.omdoc.org/physics?TemperatureUnits"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quantities.mmt#4087.122.0:4109.122.22"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/quotients.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quotients.mmt#0.0.0:418.19.0"/></metadata><mref name="[http://cds.omdoc.org/examples?LFEq]" target="http://cds.omdoc.org/examples?LFEq"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quotients.mmt#138.5.0:148.5.10"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?trivialQuotExample]" target="http://cds.omdoc.org/examples?trivialQuotExample"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/quotients.mmt#234.11.0:258.11.24"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/real.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#0.0.0:492.16.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#133.5.0:214.5.81"/></metadata>a quick, minimal definition of fractional numbers for use in quantities.mmt</opaque><mref name="[http://cds.omdoc.org/examples?Real]" target="http://cds.omdoc.org/examples?Real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#216.6.0:226.6.10"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/real.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#0.0.0:490.15.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#133.5.0:214.5.81"/></metadata>a quick, minimal definition of fractional numbers for use in quantities.mmt</opaque><mref name="[http://cds.omdoc.org/examples?Real]" target="http://cds.omdoc.org/examples?Real"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/real.mmt#216.6.0:226.6.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/sequences.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#0.0.0:1098.31.0"/></metadata><mref name="[http://cds.omdoc.org/examples?FlexaryConnectives]" target="http://cds.omdoc.org/examples?FlexaryConnectives"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#42.2.0:66.2.24"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FlexaryQuantifiers]" target="http://cds.omdoc.org/examples?FlexaryQuantifiers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#645.19.0:669.19.24"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/sequences.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#0.0.0:1095.29.0"/></metadata><mref name="[http://cds.omdoc.org/examples?FlexaryConnectives]" target="http://cds.omdoc.org/examples?FlexaryConnectives"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#42.2.0:66.2.24"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?FlexaryQuantifiers]" target="http://cds.omdoc.org/examples?FlexaryQuantifiers"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sequences.mmt#645.19.0:669.19.24"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/set.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#0.0.0:3778.66.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Sets]" target="http://cds.omdoc.org/examples?Sets"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#164.5.0:174.5.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/shallow_polymorphism.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#0.0.0:945.25.0"/></metadata><mref name="[http://cds.omdoc.org/examples?Equality]" target="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#99.3.0:113.3.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples?Lists]" target="http://cds.omdoc.org/examples?Lists"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#586.16.1:597.16.12"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/sigma.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sigma.mmt#0.0.0:992.20.0"/></metadata><mref name="[http://cds.omdoc.org/examples?DepSumChurch]" target="http://cds.omdoc.org/examples?DepSumChurch"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sigma.mmt#42.2.0:60.2.18"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/sigma.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sigma.mmt#0.0.0:990.19.0"/></metadata><mref name="[http://cds.omdoc.org/examples?DepSumChurch]" target="http://cds.omdoc.org/examples?DepSumChurch"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/sigma.mmt#42.2.0:60.2.18"/></metadata></mref></omdoc>
\ No newline at end of file
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/tutorial/1-sfol.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#0.0.0:7784.166.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#260.6.0:372.6.112"/></metadata>This file contains a definition of first-order logic in MMT as used in the MMT tutorial given at CICM 2016.</opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#376.9.0:451.9.75"/></metadata>A namespace declaration defines the root URI of the following content.</opaque><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#504.12.0:601.12.97"/></metadata>A theory defines a language. It may optionally use a meta-theory, which is given by its URI.</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?FOL]" target="http://cds.omdoc.org/examples/tutorial?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#603.13.0:612.13.9"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#4898.98.0:5062.100.0"/></metadata>Now we define the proof theory of LF using natural deduction proof rules.
It is practical to do this in a separate theory that includes the syntax above.</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?NatDed]" target="http://cds.omdoc.org/examples/tutorial?NatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#5072.101.0:5084.101.12"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#7512.160.0:7696.161.81"/></metadata>The rules declared so far only yield intuitionistic first-order logic. To get to classical logic,
we can use the modular approach and extend NatDed by the law of excluded middle:</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?ClassicalSFOL]" target="http://cds.omdoc.org/examples/tutorial?ClassicalSFOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#7698.162.0:7717.162.19"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#0.0.0:3883.101.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#51.2.0:83.2.32"/></metadata>A Semigroup consists of ...</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?Semigroup]" target="http://cds.omdoc.org/examples/tutorial?Semigroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#85.3.0:100.3.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Monoid]" target="http://cds.omdoc.org/examples/tutorial?Monoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#684.16.0:696.16.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?PreOrder]" target="http://cds.omdoc.org/examples/tutorial?PreOrder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1144.28.0:1158.28.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?MonoidAsPreorder]" target="http://cds.omdoc.org/examples/tutorial?MonoidAsPreorder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1526.40.0:1546.40.20"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Abelian]" target="http://cds.omdoc.org/examples/tutorial?Abelian"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2317.52.0:2330.52.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Group]" target="http://cds.omdoc.org/examples/tutorial?Group"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2414.58.0:2425.58.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?AbelianGroup]" target="http://cds.omdoc.org/examples/tutorial?AbelianGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2569.67.0:2587.67.18"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Ring]" target="http://cds.omdoc.org/examples/tutorial?Ring"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2643.72.0:2653.72.10"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/examples/tutorial/2-algebra.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#0.0.0:3881.100.0"/></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#51.2.0:83.2.32"/></metadata>A Semigroup consists of ...</opaque><mref name="[http://cds.omdoc.org/examples/tutorial?Semigroup]" target="http://cds.omdoc.org/examples/tutorial?Semigroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#85.3.0:100.3.15"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Monoid]" target="http://cds.omdoc.org/examples/tutorial?Monoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#684.16.0:696.16.12"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?PreOrder]" target="http://cds.omdoc.org/examples/tutorial?PreOrder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1144.28.0:1158.28.14"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?MonoidAsPreorder]" target="http://cds.omdoc.org/examples/tutorial?MonoidAsPreorder"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#1526.40.0:1546.40.20"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Abelian]" target="http://cds.omdoc.org/examples/tutorial?Abelian"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2317.52.0:2330.52.13"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Group]" target="http://cds.omdoc.org/examples/tutorial?Group"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2414.58.0:2425.58.11"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?AbelianGroup]" target="http://cds.omdoc.org/examples/tutorial?AbelianGroup"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2569.67.0:2587.67.18"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?Ring]" target="http://cds.omdoc.org/examples/tutorial?Ring"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2643.72.0:2653.72.10"/></metadata></mref></omdoc>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/examples/tutorial/3-literalsrules.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/3-literalsrules.mmt#0.0.0:2927.60.0"/></metadata><mref name="[http://cds.omdoc.org/examples/tutorial?Nat]" target="http://cds.omdoc.org/examples/tutorial?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/3-literalsrules.mmt#107.4.0:116.4.9"/></metadata></mref><mref name="[http://cds.omdoc.org/examples/tutorial?NatAsMonoid]" target="http://cds.omdoc.org/examples/tutorial?NatAsMonoid"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/3-literalsrules.mmt#2756.54.0:2771.54.15"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -6,8 +6,6 @@ Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/argumenta
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/arithmetic_rules.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/bands.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/base-arith.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/dummy.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/equivalence.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/hott.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/inductive.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/instances.omdoc
......@@ -21,7 +19,6 @@ Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/patterns.
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/program.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/programming
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/quantities.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/quotients.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/real.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/sequences.omdoc
Declares http://docs.omdoc.org/examples http://docs.omdoc.org/examples/set.omdoc
......
document http://docs.omdoc.org/examples/dummy.omdoc
Declares http://docs.omdoc.org/examples/dummy.omdoc http://cds.omdoc.org/ignore?NullPointerBugExample
document http://docs.omdoc.org/examples/equivalence.omdoc
Declares http://docs.omdoc.org/examples/equivalence.omdoc http://cds.omdoc.org/examples?LFEq
Declares http://docs.omdoc.org/examples/equivalence.omdoc http://cds.omdoc.org/examples?trivialEquivExample
theory http://cds.omdoc.org/examples?LFEq
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/mmt?Errors
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?ModExp
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/mmt?mmt
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?Typed
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?Kinded
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?TypedConstants
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?KindedConstants
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?TermsTypesKinds
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?LambdaPi
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?LFRules
Includes http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/urtheories?LF
Declares http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/examples?LFEq?[scala://structuralfeatures.lf.mmt.kwarc.info?EquivalenceRelation]
constant http://cds.omdoc.org/examples?LFEq?[scala://structuralfeatures.lf.mmt.kwarc.info?EquivalenceRelation]
Declares http://cds.omdoc.org/examples?LFEq http://cds.omdoc.org/examples?LFEq?[scala://structuralfeatures.lf.mmt.kwarc.info?Quotients]
constant http://cds.omdoc.org/examples?LFEq?[scala://structuralfeatures.lf.mmt.kwarc.info?Quotients]
datatypeconstructor http://cds.omdoc.org/examples?trivialEquivExample?true
datatypeconstructor http://cds.omdoc.org/examples?trivialEquivExample?trivial_relation
datatypeconstructor http://cds.omdoc.org/examples?trivialEquivExample?trivExam/triv_rel
dataconstructor http://cds.omdoc.org/examples?trivialEquivExample?trivExam/trans_triv_rel
dataconstructor http://cds.omdoc.org/examples?trivialEquivExample?trivExam/symm_triv_rel
dataconstructor http://cds.omdoc.org/examples?trivialEquivExample?trivExam/refl_triv_rel
theory http://cds.omdoc.org/examples?trivialEquivExample
HasMeta http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?LFEq
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?[scala://structuralfeatures.lf.mmt.kwarc.info?EquivalenceRelation]
constant http://cds.omdoc.org/examples?trivialEquivExample?[scala://structuralfeatures.lf.mmt.kwarc.info?EquivalenceRelation]
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?true
constant http://cds.omdoc.org/examples?trivialEquivExample?true
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?trivial_relation
constant http://cds.omdoc.org/examples?trivialEquivExample?trivial_relation
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?trivExam
deriveddeclaration http://cds.omdoc.org/examples?trivialEquivExample?trivExam
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?trivExam/triv_rel
constant http://cds.omdoc.org/examples?trivialEquivExample?trivExam/triv_rel
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?trivExam/trans_triv_rel
constant http://cds.omdoc.org/examples?trivialEquivExample?trivExam/trans_triv_rel
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?trivExam/symm_triv_rel
constant http://cds.omdoc.org/examples?trivialEquivExample?trivExam/symm_triv_rel
Declares http://cds.omdoc.org/examples?trivialEquivExample http://cds.omdoc.org/examples?trivialEquivExample?trivExam/refl_triv_rel
constant http://cds.omdoc.org/examples?trivialEquivExample?trivExam/refl_triv_rel
datatypeconstructor http://cds.omdoc.org/examples?trivialQuotExample?true
datatypeconstructor http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/triv_rel
datatypeconstructor http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/Q
dataconstructor http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotient_map
dataconstructor http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotInvert
dataconstructor http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotInverse
theory http://cds.omdoc.org/examples?trivialQuotExample
HasMeta http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?LFEq
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?[scala://structuralfeatures.lf.mmt.kwarc.info?EquivalenceRelation]
constant http://cds.omdoc.org/examples?trivialQuotExample?[scala://structuralfeatures.lf.mmt.kwarc.info?EquivalenceRelation]
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?[scala://structuralfeatures.lf.mmt.kwarc.info?Quotients]
constant http://cds.omdoc.org/examples?trivialQuotExample?[scala://structuralfeatures.lf.mmt.kwarc.info?Quotients]
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?true
constant http://cds.omdoc.org/examples?trivialQuotExample?true
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?trivialExam
deriveddeclaration http://cds.omdoc.org/examples?trivialQuotExample?trivialExam
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/triv_rel
constant http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/triv_rel
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/Q
constant http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/Q
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotient_map
constant http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotient_map
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotInvert
constant http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotInvert
Declares http://cds.omdoc.org/examples?trivialQuotExample http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotInverse
constant http://cds.omdoc.org/examples?trivialQuotExample?trivialExam/quotInverse
datatypeconstructor http://cds.omdoc.org/ignore?NullPointerBugExample?breaks
theory http://cds.omdoc.org/ignore?NullPointerBugExample
HasMeta http://cds.omdoc.org/ignore?NullPointerBugExample http://cds.omdoc.org/urtheories?PLF
Declares http://cds.omdoc.org/ignore?NullPointerBugExample http://cds.omdoc.org/ignore?NullPointerBugExample?breaks
constant http://cds.omdoc.org/ignore?NullPointerBugExample?breaks
document http://docs.omdoc.org/examples/quotients.omdoc
Declares http://docs.omdoc.org/examples/quotients.omdoc http://cds.omdoc.org/examples?LFEq
Declares http://docs.omdoc.org/examples/quotients.omdoc http://cds.omdoc.org/examples?trivialQuotExample
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment