]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 468da7a)
- provastruct.theory.xml removed (what was that exactly?)
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 30 Mar 2004 16:36:09 +0000 (16:36 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 30 Mar 2004 16:36:09 +0000 (16:36 +0000)
- @name of SECTION renamed to @uri

helm/dtd/provastruct.theory.xml [deleted file] patch | blob | history
helm/dtd/theoryobject.dtd patch | blob | history

diff --git a/helm/dtd/provastruct.theory.xml b/helm/dtd/provastruct.theory.xml
deleted file mode 100644 (file)
index 23c8f7c..0000000
--- a/helm/dtd/provastruct.theory.xml
+++ /dev/null
@@ -1,158 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE SECTION SYSTEM "theoryobject.dtd">
-
-<SECTION>
- 
- <SECTION>
-  <Variable name="A" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
-    <m:math><m:apply><m:csymbol>cast</m:csymbol>
-      
-        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-      
-      
-        <m:apply><m:csymbol>Type</m:csymbol></m:apply>
-      
-    </m:apply></m:math>
-  </type></Variable>
-  <SECTION>
-   <Variable name="B" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
-    <m:math><m:apply><m:csymbol>cast</m:csymbol>
-      
-        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-      
-      
-        <m:apply><m:csymbol>Type</m:csymbol></m:apply>
-      
-    </m:apply></m:math>
-  </type></Variable>
-   <Axiom name="axiom" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A 0: B</Params><type>
-    <m:math><m:apply><m:csymbol>cast</m:csymbol>
-      
-        <m:apply><m:csymbol>arrow</m:csymbol>
-            <m:ci>A</m:ci>
-          
-            <m:apply><m:csymbol>arrow</m:csymbol>
-                <m:apply><m:csymbol>arrow</m:csymbol>
-                    <m:ci>A</m:ci>
-                  
-                    <m:ci>B</m:ci>
-                  </m:apply>
-              
-                <m:ci>B</m:ci>
-              </m:apply>
-          </m:apply>
-      
-      
-        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-      
-    </m:apply></m:math>
-  </type></Axiom>
-   <Definition name="th1" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A 0: B</Params><body>
-    <m:math><m:lambda><m:bvar><m:ci>A0</m:ci><m:type>
-        <m:ci>A</m:ci>
-      </m:type></m:bvar>
-        <m:lambda><m:bvar><m:ci>H</m:ci><m:type>
-            <m:apply><m:csymbol>arrow</m:csymbol>
-                <m:ci>A</m:ci>
-              
-                <m:ci>B</m:ci>
-              </m:apply>
-          </m:type></m:bvar>
-            <m:apply><m:csymbol>app</m:csymbol>
-              <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind">conj</m:ci>
-              <m:ci>A</m:ci>
-              <m:ci>B</m:ci>
-              <m:ci>A0</m:ci>
-              <m:apply><m:csymbol>app</m:csymbol>
-                <m:ci definitionURL="cic:/prove/provastruct/a/b1/axiom.con">axiom</m:ci>
-                <m:ci>A0</m:ci>
-                <m:ci>H</m:ci>
-              </m:apply>
-            </m:apply>
-          </m:lambda>
-      </m:lambda></m:math>
-  </body><type>
-    <m:math><m:apply><m:csymbol>cast</m:csymbol>
-      
-        <m:apply><m:csymbol>arrow</m:csymbol>
-            <m:ci>A</m:ci>
-          
-            <m:apply><m:csymbol>arrow</m:csymbol>
-                <m:apply><m:csymbol>arrow</m:csymbol>
-                    <m:ci>A</m:ci>
-                  
-                    <m:ci>B</m:ci>
-                  </m:apply>
-              
-                <m:apply><m:and definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind"/><m:ci>A</m:ci><m:ci>B</m:ci></m:apply>
-              </m:apply>
-          </m:apply>
-      
-      
-        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-      
-    </m:apply></m:math>
-  </type></Definition>
-  </SECTION>
-  <SECTION>
-   <Variable name="B" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
-    <m:math><m:apply><m:csymbol>cast</m:csymbol>
-      
-        <m:apply><m:csymbol>Set</m:csymbol></m:apply>
-      
-      
-        <m:apply><m:csymbol>Type</m:csymbol></m:apply>
-      
-    </m:apply></m:math>
-  </type></Variable>
-   <Axiom name="axiom&apos;" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A</Params><type>
-    <m:math><m:apply><m:csymbol>cast</m:csymbol>
-      
-        <m:apply><m:csymbol>prod</m:csymbol><m:bvar><m:ci>A</m:ci><m:type>
-            <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-          </m:type></m:bvar>
-            <m:apply><m:csymbol>arrow</m:csymbol>
-                <m:ci>A</m:ci>
-              
-                <m:ci>A</m:ci>
-              </m:apply>
-          </m:apply>
-      
-      
-        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-      
-    </m:apply></m:math>
-  </type></Axiom>
-  </SECTION>
-  <Definition name="th1&apos;" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>0: A</Params><body>
-    <m:math><m:lambda><m:bvar><m:ci>A0</m:ci><m:type>
-        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-      </m:type></m:bvar>
-        <m:lambda><m:bvar><m:ci>H</m:ci><m:type>
-            <m:ci>A0</m:ci>
-          </m:type></m:bvar>
-            <m:ci>H</m:ci>
-          </m:lambda>
-      </m:lambda></m:math>
-  </body><type>
-    <m:math><m:apply><m:csymbol>cast</m:csymbol>
-      
-        <m:apply><m:csymbol>prod</m:csymbol><m:bvar><m:ci>A</m:ci><m:type>
-            <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-          </m:type></m:bvar>
-            <m:apply><m:csymbol>arrow</m:csymbol>
-                <m:ci>A</m:ci>
-              
-                <m:ci>A</m:ci>
-              </m:apply>
-          </m:apply>
-      
-      
-        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
-      
-    </m:apply></m:math>
-  </type></Definition>
- </SECTION>
-</SECTION>
-
-<!-- This page was served in 4037 milliseconds by Cocoon 1.7.3 -->
diff --git a/helm/dtd/theoryobject.dtd b/helm/dtd/theoryobject.dtd
index c6a43d17d9cf64a820abbd9e59cf775cb5587540..f9dd18e166f6b32e02cf801578ab557dc5ed801f 100644 (file)
--- a/helm/dtd/theoryobject.dtd
+++ b/helm/dtd/theoryobject.dtd
@@ -31,11 +31,6 @@
 <!-- Third draft: May 3 2001, Irene Schena                           -->
 <!--*****************************************************************-->
 
-<!-- DA AGGIUNGERE: 
-CONJECTURE (teo da dim)
-EXERCISE
-EXAMPLE -->
-
 <!ENTITY % cicobj SYSTEM "cicobject.dtd">
 
 %cicobj;
@@ -45,7 +40,7 @@ EXAMPLE -->
 
 <!ELEMENT ht:SECTION (%theorystructure;)>
 <!ATTLIST ht:SECTION
-          name CDATA #REQUIRED>
+          uri CDATA #REQUIRED>
 
 <!ELEMENT ht:MUTUAL (ht:DEFINITION,ht:DEFINITION+)>
 
@@ -70,13 +65,3 @@ EXAMPLE -->
 <!ATTLIST ht:VARIABLE
           uri CDATA #REQUIRED
           as (Assumption|Hypothesis|LocalDefinition) #REQUIRED>
-
-
-
-
-
-
-
-
-
-
Unnamed repository; edit this file 'description' to name the repository.