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=0d98e57693b9f5aa683ae1a667e54ba301b963d6;hb=5cc1f56f25e23f8132b578f9ad46ac9e27979cb4;hp=0000000000000000000000000000000000000000;hpb=aa12f8cd84908fb3757a582cadd36ef49e269a2b;p=helm.git

diff --git a/helm/EXPORT/exportprove/prova.v b/helm/EXPORT/exportprove/prova.v
new file mode 100644
index 000000000..0d98e5769
--- /dev/null
+++ b/helm/EXPORT/exportprove/prova.v
@@ -0,0 +1,34 @@
+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.