+++ /dev/null
-<?xml version="1.0" encoding="ISO-8859-1"?>
-
-<!-- Copyright (C) 2000, HELM Team -->
-<!-- -->
-<!-- This file is part of HELM, an Hypertextual, Electronic -->
-<!-- Library of Mathematics, developed at the Computer Science -->
-<!-- Department, University of Bologna, Italy. -->
-<!-- -->
-<!-- HELM is free software; you can redistribute it and/or -->
-<!-- modify it under the terms of the GNU General Public License -->
-<!-- as published by the Free Software Foundation; either version 2 -->
-<!-- of the License, or (at your option) any later version. -->
-<!-- -->
-<!-- HELM is distributed in the hope that it will be useful, -->
-<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
-<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
-<!-- GNU General Public License for more details. -->
-<!-- -->
-<!-- You should have received a copy of the GNU General Public License -->
-<!-- along with HELM; if not, write to the Free Software -->
-<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
-<!-- MA 02111-1307, USA. -->
-<!-- -->
-<!-- For details, see the HELM World-Wide-Web page, -->
-<!-- http://cs.unibo.it/helm/. -->
-
-<!--*****************************************************************-->
-<!-- DTD FOR the MATHEMATICAL QUERY MARKUP LANGUAGE (MathQML) -->
-<!-- First draft: April 2002, Irene Schena -->
-<!--*****************************************************************-->
-
-<!--*****************************************************************-->
-<!-- This syntax is not convenient for humans to read and write, but -->
-<!-- it is for programs. -->
-<!-- XMathQL is useful for: -->
-<!-- 1) generating queries in a XML-orienting programming environment-->
-<!-- 2) embedding queries in XML documents -->
-<!-- 3) reusing queries saved in a standard format -->
-<!-- The syntax reflects the structure of the grammar productions of -->
-<!-- MathQL. -->
-<!-- The %queryexpr parameter entity is used to allow all query -->
-<!-- expression types to occur -->
-<!-- Operators are unambiguous (binary or unary), so there isn't any -->
-<!-- grouping operator. -->
-<!-- CONST is the constant string. -->
-<!-- The attributes binder and rvar declare variables which are -->
-<!-- referred to and used by means of respectively BINDER and RVAR -->
-<!--*****************************************************************-->
-
-<!ENTITY % position '(Conclusion|Hypothesis|Body|MainConclusion|
- MainHypothesis)'>
-
-<!ENTITY % bool '(True|False)'>
-
-<!-- MathQL query expression declaration -->
-
-<!ENTITY % queryexpr '(Union|Intersect|Diff|Select|Exists|Use|UsedBy|
- ConstructorsOf|Pattern|InTheory|TheoryRefTo|TypeOf|
- SuperTypeOf|SubTypeOf|Group)'>
-
-<!-- MathQL boolean expression declaration -->
-
-<!ENTITY % boolexpr '(AND|OR|NOT|BOOL|IS|GROUP)'>
-
-<!-- MathQL string expression declaration -->
-
-<!ENTITY % functexpr '(NAME|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
-
-<!ENTITY % stringexpr '(CONST|POSITION|RVAR|BINDER|%functexpr;)'>
-
-
-<!-- MathQL top-element -->
-
-<!ELEMENT MathQL %queryexpr;>
-
-<!-- MathQL query expressions -->
-
-<!ELEMENT Union (%queryexpr;, %queryexpr;)>
-
-<!ELEMENT Intersect (%queryexpr;, %queryexpr;)>
-
-<!ELEMENT Diff (%queryexpr;, %queryexpr;)>
-
-<!ELEMENT Select (In, Where)>
-
-<!ELEMENT Exists (In, Where)>
-
-<!ELEMENT Use (%queryexpr;, Position)>
-
-<!ELEMENT Position EMPTY>
-<!ATTLIST Position
- binder CDATA #REQUIRED>
-
-<!ELEMENT UsedBy (%queryexpr;, Position)>
-
-<!ELEMENT ConstructorsOf %queryexpr;>
-
-<!ELEMENT Pattern (Prefix, TokenList, (FragmentID?))>
-
-<!ELEMENT InTheory (%queryexpr;, ItemType)>
-
-<!ELEMENT ItemType EMPTY>
-<!ATTLIST ItemType
- binder CDATA #REQUIRED>
-
-<!ELEMENT TheoryRefTo %queryexpr;>
-
-<!ELEMENT TypeOf %queryexpr;>
-<!ATTLIST TypeOf
- binder CDATA #REQUIRED>
-
-<!ELEMENT SuperTypeOf %queryexpr;>
-<!ATTLIST SuperTypeOf
- binder CDATA #REQUIRED>
-
-<!ELEMENT SubTypeOf %queryexpr;>
-<!ATTLIST SubTypeOf
- binder CDATA #REQUIRED>
-
-<!-- MathQL query sub-expressions -->
-
-<!ELEMENT In %queryexpr;>
-
-<!ELEMENT Where %boolexpr;>
-<!ATTLIST Where
- rvar CDATA #REQUIRED>
-
-<!ELEMENT STAR EMPTY>
-
-<!ELEMENT TWOSTARS EMPTY>
-
-<!ELEMENT SLASH EMPTY>
-
-<!ELEMENT QUESTIONMARK EMPTY>
-
-<!ELEMENT NUMBER EMPTY>
-<!ATTLIST NUMBER
- value NMTOKEN #REQUIRED>
-
-<!-- STAR expands only to objects of the specified dir before the last "/":
- ex. cic:/Algebra/* expands to every object in Algebra only -->
-<!-- TWOSTARS expands till the most complete name (with extension if not
- specifified) -->
-<!-- QUESTIONMARK matches one character except "/" -->
-<!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
-
-<!ELEMENT Prefix (CONST|STAR)>
-
-<!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
-<!ELEMENT FragmentID (NUMBER|TWOSTARS|STAR)+>
-
-<!-- MathQL boolean expressions -->
-
-<!ELEMENT AND (%boolexpr;, %boolexpr;)>
-
-<!ELEMENT OR (%boolexpr;, %boolexpr;)>
-
-<!ELEMENT NOT %boolexpr;>
-
-<!ELEMENT IS (%stringexpr;, %stringexpr;)>
-
-<!ELEMENT BOOL EMPTY>
-<!ATTLIST BOOL
- value %bool; #REQUIRED>
-
-<!-- MathQL string expressions -->
-
-<!ELEMENT CONST (#PCDATA)>
-
-<!ELEMENT RVAR EMPTY>
-<!ATTLIST RVAR
- name CDATA #REQUIRED>
-
-<!ELEMENT BINDER EMPTY>
-<!ATTLIST BINDER
- name CDATA #REQUIRED>
-
-<!ELEMENT POSITION EMPTY>
-<!ATTLIST POSITION
- name %position; #REQUIRED>
-
-<!ELEMENT NAME (RVAR)>
-
-<!ELEMENT PROPERTY (RVAR)>
-<!ATTLIST PROPERTY
- name CDATA #REQUIRED>
-
-<!ELEMENT SUPERPROPERTY (RVAR)>
-<!ATTLIST SUPERPROPERTY
- name CDATA #REQUIRED>
-
-<!ELEMENT SUBPROPERTY (RVAR)>
-<!ATTLIST SUBPROPERTY
- name CDATA #REQUIRED>
\ No newline at end of file
projects / helm.git / blobdiff