summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rng/omdoccth.rng
diff options
context:
space:
mode:
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.rng228
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'.
--->