Verified Commit e713a9cc authored by ColinRothgang's avatar ColinRothgang

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

parents c8bbedc8 a7d9a993
errors
*~
/narration/dummy.omdoc
/source/dummy.mmt
......@@ -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
......
......@@ -12,6 +12,8 @@ extension info.kwarc.mmt.api.archives.MWSHarvestExporter
//extension info.kwarc.mmt.api.ontology.RelationalReader
extension info.kwarc.mmt.api.ontology.AlignmentsServer
extension info.kwarc.mmt.lf.Plugin
mathpath archive ../urtheories
mathpath archive .
......@@ -93,20 +95,24 @@ define temp2
server on 8080
log+ server
log+ debug
log+ object-checker
log+ subtype-rule-gen
//log+ object-checker
//log+ object-simplifier
//log+ structure-simplifier
//log+ structure-checker
//log+ object-parser
//extension info.kwarc.mmt.lf.structuralfeatures.InductiveTypes
//log+ InductiveTypes
mathpath archive ../LFX
extension info.kwarc.mmt.odk.Plugin
mathpath archive ../../Test
mathpath archive ../../MitM
//log+ backend
extension info.kwarc.mmt.lf.structuralfeatures.InductiveTypes
log+ InductiveTypes
mathpath archive ../../Test/General
build MMT/examples mmt-omdoc inductive.mmt
build MMT/examples mmt-omdoc
//mathpath archive ../LFX
//mathpath archive ../../MitM
//mathpath archive ../../Isabelle
//gui on
end
define MMTTest
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.