diff options
Diffstat (limited to 'plugins/xml/cic.dtd')
| -rw-r--r-- | plugins/xml/cic.dtd | 259 |
1 files changed, 0 insertions, 259 deletions
diff --git a/plugins/xml/cic.dtd b/plugins/xml/cic.dtd deleted file mode 100644 index c8035cab..00000000 --- a/plugins/xml/cic.dtd +++ /dev/null @@ -1,259 +0,0 @@ -<?xml encoding="ISO-8859-1"?> - -<!-- Copyright (C) 2000-2004, 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 CIC OBJECTS: --> - -<!-- CIC term declaration --> - -<!ENTITY % term '(LAMBDA|CAST|PROD|REL|SORT|APPLY|VAR|META|IMPLICIT|CONST| - LETIN|MUTIND|MUTCONSTRUCT|MUTCASE|FIX|COFIX|instantiate)'> - -<!-- CIC sorts --> - -<!ENTITY % sort '(Prop|Set|Type|CProp)'> - -<!-- CIC sequents --> - -<!ENTITY % sequent '((Decl|Def|Hidden)*,Goal)'> - -<!-- CIC objects: --> - -<!ELEMENT ConstantType %term;> -<!ATTLIST ConstantType - name CDATA #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT ConstantBody %term;> -<!ATTLIST ConstantBody - for CDATA #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT CurrentProof (Conjecture*,body)> -<!ATTLIST CurrentProof - of CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT InductiveDefinition (InductiveType+)> -<!ATTLIST InductiveDefinition - noParams NMTOKEN #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Variable (body?,type)> -<!ATTLIST Variable - name CDATA #REQUIRED - params CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Sequent %sequent;> -<!ATTLIST Sequent - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!-- Elements used in CIC objects, which are not terms: --> - -<!ELEMENT InductiveType (arity,Constructor*)> -<!ATTLIST InductiveType - name CDATA #REQUIRED - inductive (true|false) #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Conjecture %sequent;> -<!ATTLIST Conjecture - no NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT Constructor %term;> -<!ATTLIST Constructor - name CDATA #REQUIRED> - -<!ELEMENT Decl %term;> -<!ATTLIST Decl - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Def %term;> -<!ATTLIST Def - name CDATA #IMPLIED - id ID #REQUIRED> - -<!ELEMENT Hidden EMPTY> -<!ATTLIST Hidden - id ID #REQUIRED> - -<!ELEMENT Goal %term;> - -<!-- CIC terms: --> - -<!ELEMENT LAMBDA (decl*,target)> -<!ATTLIST LAMBDA - sort %sort; #REQUIRED> - -<!ELEMENT LETIN (def*,target)> -<!ATTLIST LETIN - sort %sort; #REQUIRED> - -<!ELEMENT PROD (decl*,target)> -<!ATTLIST PROD - type %sort; #REQUIRED> - -<!ELEMENT CAST (term,type)> -<!ATTLIST CAST - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT REL EMPTY> -<!ATTLIST REL - value NMTOKEN #REQUIRED - binder CDATA #REQUIRED - id ID #REQUIRED - idref IDREF #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT SORT EMPTY> -<!ATTLIST SORT - value CDATA #REQUIRED - id ID #REQUIRED> - -<!ELEMENT APPLY (%term;)+> -<!ATTLIST APPLY - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT VAR EMPTY> -<!ATTLIST VAR - uri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- The substitutions are ordered by increasing DeBrujin --> -<!-- index. An empty substitution means that that index is --> -<!-- not accessible. --> -<!ELEMENT META (substitution*)> -<!ATTLIST META - no NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT IMPLICIT EMPTY> -<!ATTLIST IMPLICIT - id ID #REQUIRED> - -<!ELEMENT CONST EMPTY> -<!ATTLIST CONST - uri CDATA #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTIND EMPTY> -<!ATTLIST MUTIND - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED> - -<!ELEMENT MUTCONSTRUCT EMPTY> -<!ATTLIST MUTCONSTRUCT - uri CDATA #REQUIRED - noType NMTOKEN #REQUIRED - noConstr NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT MUTCASE (patternsType,inductiveTerm,pattern*)> -<!ATTLIST MUTCASE - uriType CDATA #REQUIRED - noType NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT FIX (FixFunction+)> -<!ATTLIST FIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!ELEMENT COFIX (CofixFunction+)> -<!ATTLIST COFIX - noFun NMTOKEN #REQUIRED - id ID #REQUIRED - sort %sort; #REQUIRED> - -<!-- Elements used in CIC terms: --> - -<!ELEMENT FixFunction (type,body)> -<!ATTLIST FixFunction - name CDATA #REQUIRED - id ID #REQUIRED - recIndex NMTOKEN #REQUIRED> - -<!ELEMENT CofixFunction (type,body)> -<!ATTLIST CofixFunction - id ID #REQUIRED - name CDATA #REQUIRED> - -<!ELEMENT substitution ((%term;)?)> - -<!-- Explicit named substitutions: --> - -<!ELEMENT instantiate ((CONST|MUTIND|MUTCONSTRUCT|VAR),arg+)> -<!ATTLIST instantiate - id ID #IMPLIED> - -<!-- Sintactic sugar for CIC terms and for CIC objects: --> - -<!ELEMENT arg %term;> -<!ATTLIST arg - relUri CDATA #REQUIRED> - -<!ELEMENT decl %term;> -<!ATTLIST decl - id ID #REQUIRED - type %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT def %term;> -<!ATTLIST def - id ID #REQUIRED - sort %sort; #REQUIRED - binder CDATA #IMPLIED> - -<!ELEMENT target %term;> - -<!ELEMENT term %term;> - -<!ELEMENT type %term;> - -<!ELEMENT arity %term;> - -<!ELEMENT patternsType %term;> - -<!ELEMENT inductiveTerm %term;> - -<!ELEMENT pattern %term;> - -<!ELEMENT body %term;> |