+++ /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 (XMathQL) -->
-<!-- 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. -->
-<!-- Operators are unambiguous (binary or unary), so there isn't any -->
-<!-- grouping operator. -->
-<!-- SORTBY operator for sorting query results. -->
-<!-- CONST is the constant string; rvar is for references and lvar -->
-<!-- for list. -->
-<!-- The attributes binder, rvar, lvar declare variables which are -->
-<!-- referred to and used by means of respectively BINDER, Rvar and -->
-<!-- RVAR, Lvar and LVAR. -->
-<!-- Rvar (Lvar) is casted to a list, on the contrary the use of RVAR-->
-<!-- (LVAR) is casted to a string. -->
-<!-- PROPERTY works on a specified RDF property returning its value. -->
-<!--*****************************************************************-->
-
-<!ENTITY % order '(ascendant|descendant)'>
-
-<!ENTITY % position '(MainHypothesis|Hypothesis|MainConclusion|Conclusion|
- Body)'>
-
-<!ENTITY % bool '(True|False)'>
-
-<!ENTITY % token '(CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)'>
-
-<!-- MathQL list expression declaration -->
-
-<!ENTITY % listexpr '(Rvar|Lvar|Reference|Pattern|Select|LetIn|SortBy|
- Use|UsedBy|ConstructorsOf|InTheory|TheoryRefTo|
- TypeOf|SuperTypeOf|SubTypeOf|Union|Intersect|Diff|
- Minimize)'>
-
-<!-- MathQL boolean expression declaration -->
-
-<!ENTITY % boolexpr '(BOOL|NOT|AND|OR|IS|SETEQUAL|SUBSET|EXISTS)'>
-
-<!-- MathQL string expression declaration -->
-
-<!ENTITY % functexpr '(NAME|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
-
-<!ENTITY % stringexpr '(CONST|POSITION|RVAR|BINDER|%functexpr;)'>
-
-
-<!-- MathQL query top-element -->
-
-<!ELEMENT MQLquery %listexpr;>
-
-<!-- MathQL list expressions -->
-<!ELEMENT Rvar EMPTY>
-<!ATTLIST Rvar
- name CDATA #REQUIRED>
-
-<!ELEMENT Lvar EMPTY>
-<!ATTLIST Lvar
- name CDATA #REQUIRED>
-
-<!ELEMENT Reference (RPrefix, RBody, Ext, (RFragmentID?))>
-
-<!ELEMENT Pattern (PPrefix, PBody, (Ext?), (PFragmentID?))>
-
-<!ELEMENT Select (In, Where)>
-
-<!ELEMENT LetIn (%listexpr;, Target)>
-
-<!ELEMENT Use (%listexpr;, Position)>
-
-<!ELEMENT UsedBy (%listexpr;, Position)>
-
-<!ELEMENT ConstructorsOf %listexpr;>
-
-<!ELEMENT InTheory (%listexpr;, ItemType)>
-
-<!ELEMENT TheoryRefTo %listexpr;>
-
-<!ELEMENT TypeOf %listexpr;>
-<!ATTLIST TypeOf
- binder CDATA #REQUIRED>
-
-<!ELEMENT SuperTypeOf %listexpr;>
-<!ATTLIST SuperTypeOf
- binder CDATA #REQUIRED>
-
-<!ELEMENT SubTypeOf %listexpr;>
-<!ATTLIST SubTypeOf
- binder CDATA #REQUIRED>
-
-<!ELEMENT Union (%listexpr;, %listexpr;)>
-
-<!ELEMENT Intersect (%listexpr;, %listexpr;)>
-
-<!ELEMENT Diff (%listexpr;, %listexpr;)>
-
-<!ELEMENT SortBy (%listexpr;, SortField)>
-
-<!ELEMENT Minimize %listexpr;>
-
-<!-- MathQL list sub-expressions -->
-
-<!ELEMENT RPrefix (CONST)>
-
-<!ELEMENT RBody (CONST)>
-
-<!ELEMENT RFragmentID (NUMBER)+>
-
-<!ELEMENT Ext (CONST)>
-
-<!ELEMENT PPrefix (CONST|STAR)>
-
-<!ELEMENT PBody (%token;)+>
-
-<!-- XPointers have max depth = 2 (see CIC inductive definitions) -->
-<!ELEMENT PFragmentID (NUMBER|TWOSTARS|STAR)+>
-
-<!ELEMENT NUMBER EMPTY>
-<!ATTLIST NUMBER
- value NMTOKEN #REQUIRED>
-
-<!-- We need SLASH for grouping CONST with QUESTIONMARK -->
-<!ELEMENT SLASH EMPTY>
-
-<!-- STAR expands only to objects of the specified dir before the last "/":
- ex. cic:/Algebra/* expands to every object in Algebra only -->
-<!ELEMENT STAR EMPTY>
-
-<!-- TWOSTARS expands till the most complete name (with extension if not
- specifified) -->
-<!ELEMENT TWOSTARS EMPTY>
-
-<!-- QUESTIONMARK matches one character except "/" -->
-<!ELEMENT QUESTIONMARK EMPTY>
-
-<!ELEMENT In %listexpr;>
-
-<!ELEMENT Where %boolexpr;>
-<!ATTLIST Where
- rvar CDATA #REQUIRED>
-
-<!ELEMENT Target %listexpr;>
-<!ATTLIST Target
- lvar CDATA #REQUIRED>
-
-<!ELEMENT Position EMPTY>
-<!ATTLIST Position
- binder CDATA #REQUIRED>
-
-<!ELEMENT ItemType EMPTY>
-<!ATTLIST ItemType
- binder CDATA #REQUIRED>
-
-<!ELEMENT SortField %functexpr;>
-<!ATTLIST SortField
- order %order; #IMPLIED>
-
-<!-- MathQL boolean expressions -->
-
-<!ELEMENT BOOL EMPTY>
-<!ATTLIST BOOL
- value %bool; #REQUIRED>
-
-<!ELEMENT NOT %boolexpr;>
-
-<!ELEMENT AND (%boolexpr;, %boolexpr;)>
-
-<!ELEMENT OR (%boolexpr;, %boolexpr;)>
-
-<!ELEMENT IS (%stringexpr;, %stringexpr;)>
-
-<!ELEMENT SETEQUAL (%listexpr;, %listexpr;)>
-
-<!ELEMENT SUBSET (%listexpr;, %listexpr;)>
-
-<!ELEMENT EXISTS (RVAR, %listexpr;)>
-
-<!-- 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