This commit was manufactured by cvs2svn to create branch 'moogle'.

[helm.git] / helm / papers / calculemus-2003 / slides / misc / startmusing.xml

diff --git a/helm/papers/calculemus-2003/slides/misc/startmusing.xml b/helm/papers/calculemus-2003/slides/misc/startmusing.xml
deleted file mode 100644 (file)
index 0f6cd2a..0000000
--- a/helm/papers/calculemus-2003/slides/misc/startmusing.xml
+++ /dev/null
@@ -1,113 +0,0 @@
-<?xml version="1.0"?>
-<start_musing id="X;h9@Xgt=sT|HF7owBaa+h,c[DbU5-b0"><gTopLevelStatus>
-<CurrentGoal>2</CurrentGoal>
-<ConstantType id="1" name="dummy" params="">
-  <PROD type="Prop">
-    <decl binder="x" id="i164" type="Type">
-      <CONST id="i262" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
-    </decl>
-    <target>
-      <APPLY id="i166" sort="Type">
-        <MUTIND id="i168" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
-        <CONST id="i176" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
-        <REL binder="x" id="i178" idref="i164" sort="Type" value="1"/>
-        <APPLY id="i180" sort="Type">
-          <CONST id="i182" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
-          <APPLY id="i188" sort="Type">
-            <CONST id="i190" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
-            <APPLY id="i196" sort="Type">
-              <CONST id="i198" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
-              <APPLY id="i204" sort="Type">
-                <CONST id="i206" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
-                <APPLY id="i212" sort="Type">
-                  <CONST id="i214" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
-                  <REL binder="x" id="i220" idref="i164" sort="Type" value="1"/>
-                  <CONST id="i222" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-                </APPLY>
-                <APPLY id="i224" sort="Type">
-                  <CONST id="i226" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
-                  <REL binder="x" id="i232" idref="i164" sort="Type" value="1"/>
-                  <CONST id="i234" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-                </APPLY>
-              </APPLY>
-              <CONST id="i236" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-            </APPLY>
-            <APPLY id="i238" sort="Type">
-              <CONST id="i240" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
-              <REL binder="x" id="i246" idref="i164" sort="Type" value="1"/>
-              <REL binder="x" id="i248" idref="i164" sort="Type" value="1"/>
-            </APPLY>
-          </APPLY>
-          <APPLY id="i250" sort="Type">
-            <CONST id="i252" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
-            <CONST id="i258" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-            <CONST id="i260" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-          </APPLY>
-        </APPLY>
-      </APPLY>
-    </target>
-  </PROD>
-</ConstantType>
-<CurrentProof id="1" of="cic:/dummy.con">
-  <Conjecture id="c0" no="2">
-    <Decl id="h0" name="x">
-      <CONST id="i0" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
-    </Decl>
-    <Goal>
-      <APPLY id="i2" sort="Type">
-        <MUTIND id="i4" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
-        <CONST id="i12" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
-        <REL binder="x" id="i14" idref="h0" sort="Type" value="1"/>
-        <APPLY id="i16" sort="Type">
-          <CONST id="i18" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
-          <APPLY id="i24" sort="Type">
-            <CONST id="i26" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
-            <APPLY id="i32" sort="Type">
-              <CONST id="i34" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
-              <APPLY id="i40" sort="Type">
-                <CONST id="i42" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
-                <APPLY id="i48" sort="Type">
-                  <CONST id="i50" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
-                  <REL binder="x" id="i56" idref="h0" sort="Type" value="1"/>
-                  <CONST id="i58" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-                </APPLY>
-                <APPLY id="i60" sort="Type">
-                  <CONST id="i62" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
-                  <REL binder="x" id="i68" idref="h0" sort="Type" value="1"/>
-                  <CONST id="i70" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-                </APPLY>
-              </APPLY>
-              <CONST id="i72" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-            </APPLY>
-            <APPLY id="i74" sort="Type">
-              <CONST id="i76" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
-              <REL binder="x" id="i82" idref="h0" sort="Type" value="1"/>
-              <REL binder="x" id="i84" idref="h0" sort="Type" value="1"/>
-            </APPLY>
-          </APPLY>
-          <APPLY id="i86" sort="Type">
-            <CONST id="i88" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
-            <CONST id="i94" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-            <CONST id="i96" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
-          </APPLY>
-        </APPLY>
-      </APPLY>
-    </Goal>
-  </Conjecture>
-  <body>
-    <LAMBDA sort="Prop">
-      <decl binder="x" id="i98" type="Type">
-        <CONST id="i162" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
-      </decl>
-      <target>
-        <META id="i130" no="2" sort="Prop">
-          <substitution>
-            <REL binder="x" id="i160" idref="i98" sort="Type" value="1"/>
-          </substitution>
-        </META>
-      </target>
-    </LAMBDA>
-  </body>
-</CurrentProof>
-</gTopLevelStatus>
-</start_musing>