diff options
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.rnc | 53 |
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'. - |