summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/schema/rnc/omdoc/omdocpf.rnc
blob: d10b6e896004d39a00809c1bb6194632b7b06ce1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
# A RelaxNG schema for Open Mathematical documents (OMDoc 1.3) Module PF 
# $Id: omdocpf.rnc 8958 2011-09-02 06:01:13Z kohlhase $
# $HeadURL: https://svn.omdoc.org/repos/omdoc/branches/omdoc-1.3/schema/rnc/omdocpf.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"

omdocpf.opt.content  &= proof* & proofobject*
omdoc.class          &= proof* & proofobject*

proof.attribs = toplevel.attribs & for.attrib?
proof.model = metadata.class & omtext* & symbol* & definition* & derive* & hypothesis*
proof = element proof {tref|(proof.attribs & proof.model)}

proofobject.attribs = proof.attribs
proofobject.model = metadata.class & mobj
proofobject = element proofobject {tref|(proofobject.attribs & proofobject.model)}

derive.attribs = id.attribs & attribute type {"conclusion" | "gap"}?
derive.model = mcf.class & method?
derive     = element derive {tref|(derive.attribs & derive.model)}

hypothesis.attribs =  id.attribs & attribute inductive {"yes" | "no"}?
hypothesis.model =  mcf.class
hypothesis = element hypothesis {tref|(hypothesis.attribs & hypothesis.model)}

method.attribs =  id.attribs & xref.attrib?
method.model = mobj* & premise* & proof* & proofobject*
method = element method {tref|(method.attribs & method.model)}

premise.attribs = xref.attrib & attribute rank {xsd:nonNegativeInteger}?
premise.model = empty
premise = element premise {tref|(premise.attribs & premise.model)}

# The rank of a premise specifies its importance in the inference rule. 
# Rank 0 (the default) is a real premise, whereas positive rank signifies 
# sideconditions of varying degree.