diff options
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/schema/rng/omdoccth.rng')
-rw-r--r-- | Master/texmf-dist/source/latex/stex/schema/rng/omdoccth.rng | 228 |
1 files changed, 0 insertions, 228 deletions
diff --git a/Master/texmf-dist/source/latex/stex/schema/rng/omdoccth.rng b/Master/texmf-dist/source/latex/stex/schema/rng/omdoccth.rng deleted file mode 100644 index d07a5b680dd..00000000000 --- a/Master/texmf-dist/source/latex/stex/schema/rng/omdoccth.rng +++ /dev/null @@ -1,228 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!-- - 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) ---> -<grammar ns="http://omdoc.org/ns" xmlns:omdoc="http://omdoc.org/ns" xmlns="http://relaxng.org/ns/structure/1.0"> - <define name="constitutive.class" combine="interleave"> - <zeroOrMore> - <ref name="inclusion"/> - </zeroOrMore> - </define> - <define name="imports.model" combine="interleave"> - <interleave> - <optional> - <ref name="morphism"/> - </optional> - <optional> - <attribute name="type"> - <choice> - <value>local</value> - <value>global</value> - </choice> - </attribute> - </optional> - <optional> - <attribute name="conservativity"> - <choice> - <value>conservative</value> - <value>monomorphism</value> - <value>definitional</value> - </choice> - </attribute> - </optional> - <optional> - <attribute name="conservativity-just"> - <ref name="omdocref"/> - </attribute> - </optional> - </interleave> - </define> - <define name="toplevel.attribs" combine="interleave"> - <optional> - <attribute name="generated-via"> - <ref name="omdocref"/> - </attribute> - </optional> - </define> - <define name="constitutive.attribs" combine="interleave"> - <optional> - <attribute name="generated-via"> - <ref name="omdocref"/> - </attribute> - </optional> - </define> - <define name="omdoc.class" combine="interleave"> - <interleave> - <zeroOrMore> - <ref name="theory-inclusion"/> - </zeroOrMore> - <zeroOrMore> - <ref name="axiom-inclusion"/> - </zeroOrMore> - </interleave> - </define> - <define name="theory-inclusion.justification"> - <zeroOrMore> - <ref name="obligation"/> - </zeroOrMore> - </define> - <define name="axiom-inclusion.justification"> - <zeroOrMore> - <ref name="obligation"/> - </zeroOrMore> - </define> - <define name="fromto.attrib"> - <interleave> - <ref name="from.attrib"/> - <attribute name="to"> - <ref name="omdocref"/> - </attribute> - </interleave> - </define> - <!-- attributes 'to' and 'from' are URIref --> - <define name="morphism.attribs"> - <interleave> - <ref name="id.attribs"/> - <optional> - <attribute name="hiding"> - <ref name="omdocrefs"/> - </attribute> - </optional> - <optional> - <attribute name="base"> - <ref name="omdocrefs"/> - </attribute> - </optional> - </interleave> - </define> - <define name="morphism.model"> - <optional> - <ref name="def.eq"/> - </optional> - </define> - <define name="morphism"> - <element name="morphism"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="morphism.attribs"/> - <ref name="morphism.model"/> - </interleave> - </choice> - </element> - </define> - <!-- base points to some other morphism it extends --> - <define name="inclusion.attribs"> - <interleave> - <ref name="id.attribs"/> - <attribute name="via"> - <ref name="omdocref"/> - </attribute> - </interleave> - </define> - <define name="inclusion.model"> - <empty/> - </define> - <define name="inclusion"> - <element name="inclusion"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="inclusion.attribs"/> - <ref name="inclusion.model"/> - </interleave> - </choice> - </element> - </define> - <!-- via points to a theory-inclusion --> - <define name="theory-inclusion.attribs"> - <interleave> - <ref name="toplevel.attribs"/> - <ref name="fromto.attrib"/> - </interleave> - </define> - <define name="theory-inclusion.model"> - <interleave> - <optional> - <ref name="metadata"/> - </optional> - <optional> - <ref name="morphism"/> - </optional> - <ref name="theory-inclusion.justification"/> - </interleave> - </define> - <define name="theory-inclusion"> - <element name="theory-inclusion"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="theory-inclusion.attribs"/> - <ref name="theory-inclusion.model"/> - </interleave> - </choice> - </element> - </define> - <define name="axiom-inclusion.attribs"> - <interleave> - <ref name="toplevel.attribs"/> - <ref name="fromto.attrib"/> - </interleave> - </define> - <define name="axiom-inclusion.model"> - <interleave> - <optional> - <ref name="metadata"/> - </optional> - <optional> - <ref name="morphism"/> - </optional> - <ref name="axiom-inclusion.justification"/> - </interleave> - </define> - <define name="axiom-inclusion"> - <element name="theory-inclusion"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="axiom-inclusion.attribs"/> - <ref name="axiom-inclusion.model"/> - </interleave> - </choice> - </element> - </define> - <define name="obligation.attribs"> - <interleave> - <ref name="id.attribs"/> - <attribute name="induced-by"> - <ref name="omdocref"/> - </attribute> - <attribute name="assertion"> - <ref name="omdocref"/> - </attribute> - </interleave> - </define> - <define name="obligation.model"> - <empty/> - </define> - <define name="obligation"> - <element name="obligation"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="obligation.attribs"/> - <ref name="obligation.model"/> - </interleave> - </choice> - </element> - </define> -</grammar> -<!-- - attribute 'assertion' is a URIref, points to an assertion - that is the proof obligation induced by the axiom or definition - specified by 'induced-by'. ---> |