Big commit and major code clean-up:

[helm.git] / helm / matita / tests / match.ma

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index c75d4fda865ecc527962c94123506bbb2a7638eb..bc8caa22332b5c4a18bb65e7a941def31f2e47c8 100644 (file)
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -1,14 +1,14 @@
 (**************************************************************************)
-(*       ___                                                             *)
+(*       ___                                                               *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *) 
-(*      ||I||       Developers:                                           *) 
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
 (*      \   /                                                             *)
 (*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU Lesser General Public License Version 2.1         *)   
+(*        v         GNU Lesser General Public License Version 2.1         *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -19,10 +19,10 @@ I : True.
 inductive False: Prop \def .
 
 definition Not: Prop \to Prop \def
-\lambda A:Prop. (A \to False).
+\lambda A. (A \to False).
 
 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
-intros.cut False.elim Hcut.apply H1.assumption.
+intros. elim (H1 H).
 qed.
 
 inductive And (A,B:Prop) : Prop \def
@@ -295,6 +295,7 @@ simplify.apply le_n_S.apply H.
 simplify.intros.apply H.apply le_S_n.assumption.
 qed.
 
+(*CSC: this requires too much time
 theorem prova :
 let three \def (S (S (S O))) in
 let nine \def (times three three) in
@@ -304,6 +305,5 @@ let square \def (times eightyone eightyone) in
 intro.
 intro.
 intro.intro.
-STOP normalize goal at (? ? % ?).
-
-
+normalize goal at (? ? % ?).
+*)
\ No newline at end of file