diff options
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng')
| -rw-r--r-- | Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng | 634 |
1 files changed, 0 insertions, 634 deletions
diff --git a/Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng b/Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng deleted file mode 100644 index 59e54d0f723..00000000000 --- a/Master/texmf-dist/source/latex/stex/schema/rng/omdocst.rng +++ /dev/null @@ -1,634 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<!-- - A RelaxNG schema for Open Mathematical documents (OMDoc 1.3) Module ST - $Id: omdocst.rnc 8972 2011-09-09 11:36:34Z kohlhase $ - $HeadURL: https://svn.omdoc.org/repos/omdoc/branches/omdoc-1.3/schema/rnc/omdocst.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:a="http://relaxng.org/ns/compatibility/annotations/1.0" xmlns="http://relaxng.org/ns/structure/1.0" datatypeLibrary="http://www.w3.org/2001/XMLSchema-datatypes"> - <define name="omdoc.class" combine="interleave"> - <interleave> - <zeroOrMore> - <ref name="symbol"/> - </zeroOrMore> - <zeroOrMore> - <ref name="axiom"/> - </zeroOrMore> - <zeroOrMore> - <ref name="definition"/> - </zeroOrMore> - <zeroOrMore> - <ref name="imports"/> - </zeroOrMore> - <zeroOrMore> - <ref name="assertion"/> - </zeroOrMore> - <zeroOrMore> - <ref name="type"/> - </zeroOrMore> - <zeroOrMore> - <ref name="alternative"/> - </zeroOrMore> - <zeroOrMore> - <ref name="example"/> - </zeroOrMore> - <zeroOrMore> - <ref name="theory"/> - </zeroOrMore> - </interleave> - </define> - <define name="constitutive.attribs"> - <interleave> - <ref name="id.attribs"/> - <optional> - <attribute name="generated-from"> - <ref name="omdocref"/> - </attribute> - </optional> - </interleave> - </define> - <define name="sym.role.attrib"> - <attribute name="role"> - <choice> - <value>type</value> - <value>sort</value> - <value>object</value> - <value>binder</value> - <value>attribution</value> - <value>application</value> - <value>constant</value> - <value>semantic-attribution</value> - <value>error</value> - </choice> - </attribute> - </define> - <define name="theory-unique"> - <data type="NCName"/> - </define> - <define name="scope.attrib"> - <optional> - <attribute name="scope"> - <choice> - <value>global</value> - <value>local</value> - </choice> - </attribute> - </optional> - </define> - <define name="symbol.attribs"> - <interleave> - <ref name="scope.attrib"/> - <optional> - <attribute name="name"> - <ref name="theory-unique"/> - </attribute> - </optional> - <ref name="constitutive.attribs"/> - <optional> - <ref name="sym.role.attrib"/> - </optional> - </interleave> - </define> - <define name="symbol.model"> - <interleave> - <ref name="metadata.class"/> - <zeroOrMore> - <ref name="type"/> - </zeroOrMore> - </interleave> - </define> - <define name="symbol"> - <element name="symbol"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="symbol.attribs"/> - <ref name="symbol.model"/> - </interleave> - </choice> - </element> - </define> - <define name="forname.attrib"> - <attribute name="for"> - <list> - <oneOrMore> - <data type="NCName"/> - </oneOrMore> - </list> - </attribute> - </define> - <define name="axiom.attribs"> - <interleave> - <ref name="constitutive.attribs"/> - <ref name="forname.attrib"/> - <optional> - <attribute name="type"> - <data type="string"/> - </attribute> - </optional> - </interleave> - </define> - <define name="axiom.model"> - <interleave> - <ref name="metadata.class"/> - <ref name="mcf.class"/> - </interleave> - </define> - <define name="axiom"> - <element name="axiom"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="axiom.attribs"/> - <ref name="axiom.model"/> - </interleave> - </choice> - </element> - </define> - <!-- informal definitions --> - <define name="def.informal"> - <optional> - <attribute name="type"> - <value>informal</value> - </attribute> - </optional> - </define> - <!-- simple definitions --> - <define name="def.simple.attribs"> - <attribute name="type"> - <value>simple</value> - </attribute> - </define> - <define name="def.simple"> - <interleave> - <ref name="def.simple.attribs"/> - <ref name="mobj"/> - </interleave> - </define> - <!-- implicit definitions --> - <define name="exists.attrib"> - <attribute name="existence"> - <ref name="omdocref"/> - </attribute> - </define> - <define name="unique.attrib"> - <attribute name="uniqueness"> - <ref name="omdocref"/> - </attribute> - </define> - <define name="def.implicit.attribs"> - <interleave> - <attribute name="type"> - <value>implicit</value> - </attribute> - <optional> - <ref name="exists.attrib"/> - </optional> - <optional> - <ref name="unique.attrib"/> - </optional> - </interleave> - </define> - <define name="def.implicit"> - <interleave> - <ref name="def.implicit.attribs"/> - <zeroOrMore> - <ref name="FMP"/> - </zeroOrMore> - </interleave> - </define> - <define name="exhaust.attrib"> - <attribute name="exhaustivity"> - <ref name="omdocref"/> - </attribute> - </define> - <define name="consist.attrib"> - <attribute name="consistency"> - <ref name="omdocref"/> - </attribute> - </define> - <define name="def.pattern.attribs"> - <interleave> - <optional> - <attribute name="type"> - <value>pattern</value> - </attribute> - </optional> - <optional> - <ref name="exhaust.attrib"/> - </optional> - <optional> - <ref name="consist.attrib"/> - </optional> - </interleave> - </define> - <define name="def.pattern.model"> - <zeroOrMore> - <ref name="requation"/> - </zeroOrMore> - </define> - <define name="def.pattern"> - <interleave> - <ref name="def.pattern.attribs"/> - <ref name="def.pattern.model"/> - </interleave> - </define> - <define name="def.inductive.attribs"> - <interleave> - <optional> - <attribute name="type"> - <value>inductive</value> - </attribute> - </optional> - <optional> - <ref name="exhaust.attrib"/> - </optional> - <optional> - <ref name="consist.attrib"/> - </optional> - </interleave> - </define> - <define name="def.inductive.model"> - <interleave> - <zeroOrMore> - <ref name="requation"/> - </zeroOrMore> - <optional> - <ref name="measure"/> - </optional> - <optional> - <ref name="ordering"/> - </optional> - </interleave> - </define> - <define name="def.inductive"> - <interleave> - <ref name="def.inductive.attribs"/> - <ref name="def.inductive.model"/> - </interleave> - </define> - <define name="def.eq"> - <choice> - <ref name="def.pattern"/> - <ref name="def.inductive"/> - </choice> - </define> - <!-- all definition forms, add more by extending this. --> - <define name="defs.all"> - <choice> - <ref name="def.informal"/> - <ref name="def.simple"/> - <ref name="def.implicit"/> - <ref name="def.eq"/> - </choice> - </define> - <!-- - Definitions contain CMPs, FMPs and concept specifications. - The latter define the set of concepts defined in this element. - They can be reached under this name in the content dictionary - of the name specified in the theory attribute of the definition. - --> - <define name="definition.attribs"> - <interleave> - <ref name="constitutive.attribs"/> - <ref name="forname.attrib"/> - </interleave> - </define> - <define name="definition"> - <element name="definition"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="definition.attribs"/> - <ref name="mc.class"/> - <ref name="defs.all"/> - </interleave> - </choice> - </element> - </define> - <define name="requation.attribs"> - <ref name="id.attribs"/> - </define> - <define name="requation.model"> - <ref name="mobj"/> - <ref name="mobj"/> - </define> - <define name="requation"> - <element name="requation"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="requation.attribs"/> - <ref name="requation.model"/> - </interleave> - </choice> - </element> - </define> - <define name="measure.attribs"> - <ref name="id.attribs"/> - </define> - <define name="measure.model"> - <ref name="mobj"/> - </define> - <define name="measure"> - <element name="measure"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="measure.attribs"/> - <ref name="measure.model"/> - </interleave> - </choice> - </element> - </define> - <define name="ordering.attribs"> - <interleave> - <ref name="id.attribs"/> - <optional> - <attribute name="terminating"> - <ref name="omdocref"/> - </attribute> - </optional> - </interleave> - </define> - <define name="ordering.model"> - <ref name="mobj"/> - </define> - <define name="ordering"> - <element name="ordering"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="ordering.attribs"/> - <ref name="ordering.model"/> - </interleave> - </choice> - </element> - </define> - <!-- the non-constitutive statements, they need a theory attribute --> - <define name="toplevel.attribs" combine="interleave"> - <optional> - <attribute name="theory"> - <ref name="omdocref"/> - </attribute> - </optional> - </define> - <define name="ded.status.class"> - <choice> - <value>satisfiable</value> - <value>counter-satisfiable</value> - <value>no-consequence</value> - <value>theorem</value> - <value>conter-theorem</value> - <value>contradictory-axioms</value> - <value>tautologous-conclusion</value> - <value> tautology</value> - <value>equivalent</value> - <value>conunter-equivalent</value> - <value>unsatisfiable-conclusion</value> - <value>unsatisfiable</value> - </choice> - </define> - <define name="just-by.attrib"> - <attribute name="just-by"> - <ref name="omdocref"/> - </attribute> - </define> - <define name="assertion.attribs"> - <interleave> - <ref name="toplevel.attribs"/> - <optional> - <attribute name="type"> - <ref name="assertiontype"/> - </attribute> - </optional> - <optional> - <attribute name="status"> - <ref name="ded.status.class"/> - </attribute> - </optional> - <optional> - <ref name="just-by.attrib"/> - </optional> - </interleave> - </define> - <define name="assertion.model"> - <ref name="mcf.class"/> - </define> - <define name="assertion"> - <element name="assertion"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="assertion.attribs"/> - <ref name="assertion.model"/> - </interleave> - </choice> - </element> - </define> - <!-- - the assertiontype has no formal meaning yet, it is solely for human consumption. - 'just-by' is a list of URIRefs that point to proof objects, etc that justifies the status. - --> - <define name="type.attribs"> - <interleave> - <ref name="toplevel.attribs"/> - <optional> - <ref name="just-by.attrib"/> - </optional> - <optional> - <attribute name="system"> - <ref name="omdocref"/> - </attribute> - </optional> - <optional> - <attribute name="for"> - <ref name="omdocref"/> - </attribute> - </optional> - </interleave> - </define> - <define name="type.model"> - <ref name="mc.class"/> - <ref name="mobj"/> - <optional> - <ref name="mobj"/> - </optional> - </define> - <define name="type"> - <element name="type"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="type.attribs"/> - <ref name="type.model"/> - </interleave> - </choice> - </element> - </define> - <define name="alternative.attribs"> - <a:documentation>just-by, points to the theorem justifying well-definedness -entailed-by, entails, point to other (equivalent definitions -entailed-by-thm, entails-thm point to the theorems justifying -the entailment relation)</a:documentation> - <interleave> - <ref name="toplevel.attribs"/> - <ref name="for.attrib"/> - <choice> - <group> - <attribute name="equivalence"> - <ref name="omdocref"/> - </attribute> - <attribute name="equivalence-thm"> - <ref name="omdocref"/> - </attribute> - </group> - <interleave> - <attribute name="entailed-by"> - <ref name="omdocref"/> - </attribute> - <attribute name="entails"> - <ref name="omdocref"/> - </attribute> - <attribute name="entailed-by-thm"> - <ref name="omdocref"/> - </attribute> - <attribute name="entails-thm"> - <ref name="omdocref"/> - </attribute> - </interleave> - </choice> - </interleave> - </define> - <define name="alternative.model"> - <interleave> - <ref name="mc.class"/> - <ref name="defs.all"/> - </interleave> - </define> - <define name="alternative"> - <element name="alternative"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="alternative.attribs"/> - <ref name="alternative.model"/> - </interleave> - </choice> - </element> - </define> - <define name="example.attribs"> - <interleave> - <ref name="toplevel.attribs"/> - <ref name="for.attrib"/> - <optional> - <attribute name="type"> - <choice> - <value>for</value> - <value>against</value> - </choice> - </attribute> - </optional> - <optional> - <attribute name="assertion"> - <ref name="omdocref"/> - </attribute> - </optional> - </interleave> - </define> - <define name="example.model"> - <ref name="mc.class"/> - <zeroOrMore> - <ref name="mobj"/> - </zeroOrMore> - </define> - <define name="example"> - <element name="example"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="example.attribs"/> - <ref name="example.model"/> - </interleave> - </choice> - </element> - </define> - <define name="theory.attribs"> - <interleave> - <ref name="id.attribs"/> - <optional> - <attribute name="cdurl"> - <data type="anyURI"/> - </attribute> - </optional> - <optional> - <attribute name="cdbase"> - <data type="anyURI"/> - </attribute> - </optional> - <optional> - <attribute name="cdreviewdate"> - <data type="date"/> - </attribute> - </optional> - <optional> - <attribute name="cdversion"> - <data type="nonNegativeInteger"/> - </attribute> - </optional> - <optional> - <attribute name="cdrevision"> - <data type="nonNegativeInteger"/> - </attribute> - </optional> - <optional> - <attribute name="cdstatus"> - <choice> - <value>official</value> - <value>experimental</value> - <value>private</value> - <value>obsolete</value> - </choice> - </attribute> - </optional> - </interleave> - </define> - <define name="theory.model"> - <interleave> - <ref name="metadata.class"/> - <ref name="omdoc.class"/> - </interleave> - </define> - <define name="theory"> - <element name="theory"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="theory.attribs"/> - <ref name="theory.model"/> - </interleave> - </choice> - </element> - </define> - <define name="imports.attribs"> - <interleave> - <ref name="id.attribs"/> - <ref name="from.attrib"/> - </interleave> - </define> - <define name="imports.model"> - <ref name="metadata.class"/> - </define> - <define name="imports"> - <element name="imports"> - <choice> - <ref name="tref"/> - <interleave> - <ref name="imports.attribs"/> - <ref name="imports.model"/> - </interleave> - </choice> - </element> - </define> -</grammar> |