]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/dtd/provastruct.theory.xml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
This commit was manufactured by cvs2svn to create branch
[helm.git] / helm / dtd / provastruct.theory.xml
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 -->
Unnamed repository; edit this file 'description' to name the repository.