From: Enrico Tassi Date: Mon, 11 Jul 2005 14:10:43 +0000 (+0000) Subject: fix X-Git-Tag: pre_notation~42 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f7cb5462119ce44becf0bc9848d61690a048ac7;p=helm.git fix --- diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma index e53d315f0..0fcf73cf3 100644 --- a/helm/matita/tests/apply.ma +++ b/helm/matita/tests/apply.ma @@ -18,8 +18,8 @@ alias symbol "eq" (instance 0) = "leibnitz's equality". theorem a: \forall A:Set. - \forall x,y : A. - not (x=y) \to not (x=y). + \forall x: A. + not (x=x) \to not (x=x). intros. apply H. qed. diff --git a/helm/matita/tests/clearbody.ma b/helm/matita/tests/clearbody.ma index b38de22db..29dd2457d 100644 --- a/helm/matita/tests/clearbody.ma +++ b/helm/matita/tests/clearbody.ma @@ -19,7 +19,7 @@ alias symbol "plus" (instance 0) = "natural plus". theorem stupid : - let x \def 0 + 1 in x + 1= x + 1. + let x \def 0 + 1 in x + 2 = x + 2. intros. clearbody x. simplify. diff --git a/helm/matita/tests/constructor.ma b/helm/matita/tests/constructor.ma index 3b9c21c81..5f9bed6c0 100644 --- a/helm/matita/tests/constructor.ma +++ b/helm/matita/tests/constructor.ma @@ -17,6 +17,6 @@ alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "leibnitz's equality". -theorem stupid: 0 = 0. +theorem stupid: 1 = 1. constructor 1. qed. diff --git a/helm/matita/tests/contradiction.ma b/helm/matita/tests/contradiction.ma index ddd9ac878..d5199aefc 100644 --- a/helm/matita/tests/contradiction.ma +++ b/helm/matita/tests/contradiction.ma @@ -20,7 +20,7 @@ alias symbol "eq" (instance 0) = "leibnitz's equality". -theorem stupid: \forall a:Prop. a \to not a \to 0 = 1. +theorem stupid: \forall a:Prop. a \to not a \to 0 = 2. intros. letin H \def (H1 H). contradiction. diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma index 8ba63bd8b..82d36667b 100644 --- a/helm/matita/tests/cut.ma +++ b/helm/matita/tests/cut.ma @@ -16,8 +16,8 @@ set "baseuri" "cic:/matita/tests/cut". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "leibnitz's equality". -theorem stupid: 0 = 0. - cut 0 = 0. +theorem stupid: 3 = 3. + cut 3 = 3. assumption. reflexivity. qed.