X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexportprove%2Fprova.v;fp=helm%2FEXPORT%2Fexportprove%2Fprova.v;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=0d98e57693b9f5aa683ae1a667e54ba301b963d6;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git

diff --git a/helm/EXPORT/exportprove/prova.v b/helm/EXPORT/exportprove/prova.v
deleted file mode 100644
index 0d98e5769..000000000
--- a/helm/EXPORT/exportprove/prova.v
+++ /dev/null
@@ -1,34 +0,0 @@
-Require Export Xml.
-
-Section prova.
-
-Inductive
- tree : Set := node : forest -> tree
-with
- forest : Set := leaf : forest | cons : tree -> forest -> forest.
-
-Fixpoint tree_size [t:tree] : nat :=
- Cases t of (node f) => (S (forest_size f)) end
-with forest_size [f:forest] : nat :=
- Cases f of leaf => (S O) | (cons t f') => (plus (tree_size t) (forest_size f'))
- end.
-
-Theorem a_ab_b: (A,B:Prop)A->(A->B)->B.
-Auto.
-Qed.
-
-Axiom dummy_axiom: (n,m:nat)(le n m)\/(gt n m).
-
-End prova.
-
-Print XML Section Disk "examples/prove" prova.
-
-Theorem ab_ac_abc: (A,B,C:Prop)(A->B)->(A->C)->A->B/\C.
-Intros A B C AB AC A1.
-Split.
-
-Show XML File "examples/ab_ac_abc.xml" Proof.
-
-Auto.
-Auto.
-Qed.