summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdoccth.rnc
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdoccth.rnc')
-rw-r--r--Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdoccth.rnc53
1 files changed, 0 insertions, 53 deletions
diff --git a/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdoccth.rnc b/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdoccth.rnc
deleted file mode 100644
index 8e52773b51d..00000000000
--- a/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdoccth.rnc
+++ /dev/null
@@ -1,53 +0,0 @@
-# A RelaxNG schema for Open Mathematical documents (OMDoc 1.3) Module CTH
-# $Id: omdoccth.rnc 8979 2011-11-29 04:56:59Z kohlhase $
-# $HeadURL: https://svn.omdoc.org/repos/omdoc/branches/omdoc-1.3/schema/rnc/omdoccth.rnc $
-# See the documentation and examples at http://www.omdoc.org
-# Copyright (c) 2004-2007 Michael Kohlhase, released under the GNU Public License (GPL)
-
-default namespace omdoc = "http://omdoc.org/ns"
-
-constitutive.class &= inclusion*
-imports.model &= morphism? &
- attribute type { "local" | "global"}? &
- attribute conservativity {"conservative" | "monomorphism" | "definitional"}? &
- attribute conservativity-just {omdocref}?
-
-toplevel.attribs &= attribute generated-via {omdocref}?
-constitutive.attribs &= attribute generated-via {omdocref}?
-
-omdoc.class &= theory-inclusion* & axiom-inclusion*
-theory-inclusion.justification = obligation*
-axiom-inclusion.justification = obligation*
-
-fromto.attrib = from.attrib & attribute to {omdocref}
-# attributes 'to' and 'from' are URIref
-
-morphism.attribs = id.attribs &
- attribute hiding {omdocrefs}? &
- attribute base {omdocrefs}?
-morphism.model = def.eq?
-morphism = element morphism {tref|(morphism.attribs & morphism.model)}
-# base points to some other morphism it extends
-
-inclusion.attribs = id.attribs & attribute via {omdocref}
-inclusion.model = empty
-inclusion = element inclusion {tref|(inclusion.attribs & inclusion.model)}
-# via points to a theory-inclusion
-
-theory-inclusion.attribs = toplevel.attribs & fromto.attrib
-theory-inclusion.model = metadata? & morphism? & theory-inclusion.justification
-theory-inclusion = element theory-inclusion {tref|(theory-inclusion.attribs & theory-inclusion.model)}
-
-axiom-inclusion.attribs = toplevel.attribs & fromto.attrib
-axiom-inclusion.model = metadata? & morphism? & axiom-inclusion.justification
-axiom-inclusion = element theory-inclusion {tref|(axiom-inclusion.attribs & axiom-inclusion.model)}
-
-obligation.attribs = id.attribs &
- attribute induced-by {omdocref} &
- attribute assertion {omdocref}
-obligation.model = empty
-obligation = element obligation {tref|(obligation.attribs & obligation.model)}
-# attribute 'assertion' is a URIref, points to an assertion
-# that is the proof obligation induced by the axiom or definition
-# specified by 'induced-by'.
-