From: Claudio Sacerdoti Coen Date: Tue, 26 Jul 2005 17:12:34 +0000 (+0000) Subject: "Coq's " prefix added to every interpretation. X-Git-Tag: V_0_7_2~55 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cec61c8b027b15b98d308cee8900d9cf35a02d28;p=helm.git "Coq's " prefix added to every interpretation. --- diff --git a/helm/matita/tests/absurd.ma b/helm/matita/tests/absurd.ma index f5f27f622..24d2d885f 100644 --- a/helm/matita/tests/absurd.ma +++ b/helm/matita/tests/absurd.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/tests/absurd/". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "not" = "cic:/Coq/Init/Logic/not.con". diff --git a/helm/matita/tests/apply.ma b/helm/matita/tests/apply.ma index 0fcf73cf3..41bdd3afc 100644 --- a/helm/matita/tests/apply.ma +++ b/helm/matita/tests/apply.ma @@ -14,7 +14,7 @@ qed. (* test _without_ the WHD on the apply argument *) -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a: \forall A:Set. diff --git a/helm/matita/tests/assumption.ma b/helm/matita/tests/assumption.ma index 711e35cf0..4679ea1c3 100644 --- a/helm/matita/tests/assumption.ma +++ b/helm/matita/tests/assumption.ma @@ -16,9 +16,9 @@ set "baseuri" "cic:/matita/tests/assumption". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". -alias symbol "and" (instance 0) = "logical and". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". +alias symbol "and" (instance 0) = "Coq's logical and". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". theorem stupid: diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma index 66b973cfd..e7e59554c 100755 --- a/helm/matita/tests/auto.ma +++ b/helm/matita/tests/auto.ma @@ -3,10 +3,10 @@ set "baseuri" "cic:/matita/tests/auto/". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "minus" (instance 0) = "natural minus". -alias symbol "plus" (instance 0) = "natural plus". -alias symbol "times" (instance 0) = "natural times". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "minus" (instance 0) = "Coq's natural minus". +alias symbol "plus" (instance 0) = "Coq's natural plus". +alias symbol "times" (instance 0) = "Coq's natural times". theorem a : \forall x,y:nat. x*x+(S y) = O - x. intros. auto depth = 3. diff --git a/helm/matita/tests/change.ma b/helm/matita/tests/change.ma index ea894c28e..199ce3bd8 100644 --- a/helm/matita/tests/change.ma +++ b/helm/matita/tests/change.ma @@ -14,8 +14,8 @@ set "baseuri" "cic:/matita/tests/change/". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". theorem stupid: @@ -26,4 +26,4 @@ intros. change in \vdash (? ? % ?) with 5. rewrite < H in \vdash (? ? % ?). reflexivity. -qed. \ No newline at end of file +qed. diff --git a/helm/matita/tests/clear.ma b/helm/matita/tests/clear.ma index 1fe721d59..24bb3377c 100644 --- a/helm/matita/tests/clear.ma +++ b/helm/matita/tests/clear.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/tests/clear". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". diff --git a/helm/matita/tests/clearbody.ma b/helm/matita/tests/clearbody.ma index 29dd2457d..9a125e687 100644 --- a/helm/matita/tests/clearbody.ma +++ b/helm/matita/tests/clearbody.ma @@ -14,8 +14,8 @@ set "baseuri" "cic:/matita/tests/clearbody". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". theorem stupid : diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index 2444b1d74..5c157368d 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -26,7 +26,7 @@ coercion pos2nat. coercion nat2int. definition fst \def \lambda x,y:int.x. -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a: fst O one = fst (positive O) (next one). reflexivity. diff --git a/helm/matita/tests/comments.ma b/helm/matita/tests/comments.ma index cd21535e7..e9caa7edc 100644 --- a/helm/matita/tests/comments.ma +++ b/helm/matita/tests/comments.ma @@ -19,7 +19,7 @@ set "baseuri" "cic:/matita/tests/comments/". *) alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:0=0. (* nota *) diff --git a/helm/matita/tests/constructor.ma b/helm/matita/tests/constructor.ma index 5f9bed6c0..0cd22d35b 100644 --- a/helm/matita/tests/constructor.ma +++ b/helm/matita/tests/constructor.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/tests/constructor". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem stupid: 1 = 1. diff --git a/helm/matita/tests/contradiction.ma b/helm/matita/tests/contradiction.ma index d5199aefc..e4519ec3e 100644 --- a/helm/matita/tests/contradiction.ma +++ b/helm/matita/tests/contradiction.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/tests/contradiction". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/helm/matita/tests/cut.ma b/helm/matita/tests/cut.ma index 82d36667b..f5850e576 100644 --- a/helm/matita/tests/cut.ma +++ b/helm/matita/tests/cut.ma @@ -14,11 +14,11 @@ set "baseuri" "cic:/matita/tests/cut". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem stupid: 3 = 3. cut 3 = 3. assumption. reflexivity. qed. - \ No newline at end of file + diff --git a/helm/matita/tests/decompose.ma b/helm/matita/tests/decompose.ma index 48477f3eb..0b5ef7a80 100644 --- a/helm/matita/tests/decompose.ma +++ b/helm/matita/tests/decompose.ma @@ -13,8 +13,8 @@ (**************************************************************************) set "baseuri" "cic:/matita/tests/decompose". -alias symbol "and" (instance 0) = "logical and". -alias symbol "or" (instance 0) = "logical or". +alias symbol "and" (instance 0) = "Coq's logical and". +alias symbol "or" (instance 0) = "Coq's logical or". diff --git a/helm/matita/tests/discriminate.ma b/helm/matita/tests/discriminate.ma index ca55591ee..f94624567 100644 --- a/helm/matita/tests/discriminate.ma +++ b/helm/matita/tests/discriminate.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/tests/discriminate". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem stupid: diff --git a/helm/matita/tests/elim.ma b/helm/matita/tests/elim.ma index cf4e1eb22..ab7afafa6 100644 --- a/helm/matita/tests/elim.ma +++ b/helm/matita/tests/elim.ma @@ -19,9 +19,9 @@ inductive stupidtype: Set \def | Next : stupidtype \to stupidtype | Pair : stupidtype \to stupidtype \to stupidtype. -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "exists" (instance 0) = "exists". -alias symbol "or" (instance 0) = "logical or". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "exists" (instance 0) = "Coq's exists". +alias symbol "or" (instance 0) = "Coq's logical or". alias num (instance 0) = "natural number". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)". diff --git a/helm/matita/tests/fguidi.ma b/helm/matita/tests/fguidi.ma index bfd24e591..07e7989ce 100644 --- a/helm/matita/tests/fguidi.ma +++ b/helm/matita/tests/fguidi.ma @@ -10,9 +10,9 @@ alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)". alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". -alias symbol "and" (instance 0) = "logical and". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "exists" (instance 0) = "exists". +alias symbol "and" (instance 0) = "Coq's logical and". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "exists" (instance 0) = "Coq's exists". definition is_S: nat \to Prop \def \lambda n. match n with diff --git a/helm/matita/tests/fold.ma b/helm/matita/tests/fold.ma index f2f26a849..7b91c5b24 100644 --- a/helm/matita/tests/fold.ma +++ b/helm/matita/tests/fold.ma @@ -1,8 +1,8 @@ set "baseuri" "cic:/matita/tests/fold". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". theorem t: \forall x:nat. 0+x=x. intro. simplify in match (0+x) in \vdash (? ? % ?). diff --git a/helm/matita/tests/generalize.ma b/helm/matita/tests/generalize.ma index a6e56ef3e..4fe9af340 100644 --- a/helm/matita/tests/generalize.ma +++ b/helm/matita/tests/generalize.ma @@ -15,8 +15,8 @@ set "baseuri" "cic:/matita/generalize". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". @@ -33,4 +33,4 @@ qed. theorem test2: \forall x. x + 4 = 4 + x. generalize in match 4. exact plus_comm. -qed. \ No newline at end of file +qed. diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma index c76851f59..99e18012d 100644 --- a/helm/matita/tests/inversion.ma +++ b/helm/matita/tests/inversion.ma @@ -8,7 +8,7 @@ inductive le (n:nat) : nat \to Prop \def leO : le n n | leS : \forall m. le n m \to le n (S m). -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem test_inversion: \forall n. le n O \to n=O. intros. diff --git a/helm/matita/tests/paramodulation.ma b/helm/matita/tests/paramodulation.ma index b56c0da27..80a39fa3f 100644 --- a/helm/matita/tests/paramodulation.ma +++ b/helm/matita/tests/paramodulation.ma @@ -14,10 +14,10 @@ set "baseuri" "cic:/matita/tests/paramodulation". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". alias num (instance 0) = "natural number". -alias symbol "times" (instance 0) = "natural times". +alias symbol "times" (instance 0) = "Coq's natural times". theorem para1: \forall n,m,n1,m1:nat. diff --git a/helm/matita/tests/replace.ma b/helm/matita/tests/replace.ma index d209e97d4..d70a7af60 100644 --- a/helm/matita/tests/replace.ma +++ b/helm/matita/tests/replace.ma @@ -1,9 +1,9 @@ set "baseuri" "cic:/matita/tests/replace/". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". -alias symbol "times" (instance 0) = "natural times". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". +alias symbol "times" (instance 0) = "Coq's natural times". alias id "mult_n_O" = "cic:/Coq/Init/Peano/mult_n_O.con". alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". diff --git a/helm/matita/tests/rewrite.ma b/helm/matita/tests/rewrite.ma index aa4fa1f32..71a7514fa 100644 --- a/helm/matita/tests/rewrite.ma +++ b/helm/matita/tests/rewrite.ma @@ -2,8 +2,8 @@ set "baseuri" "cic:/matita/tests/rewrite/". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". -alias symbol "plus" (instance 0) = "natural plus". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". +alias symbol "plus" (instance 0) = "Coq's natural plus". alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". theorem a: @@ -31,4 +31,4 @@ qed. theorem foo: \forall n. n = n + 0. intros. rewrite < t; reflexivity. -qed. \ No newline at end of file +qed. diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma index 3edc4cf35..61d5b1163 100644 --- a/helm/matita/tests/simpl.ma +++ b/helm/matita/tests/simpl.ma @@ -1,7 +1,7 @@ set "baseuri" "cic:/matita/tests/simpl/". alias id "not" = "cic:/Coq/Init/Logic/not.con". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a : \forall A:Set. \forall x,y : A. diff --git a/helm/matita/tests/test2.ma b/helm/matita/tests/test2.ma index cf2656710..1adf17326 100644 --- a/helm/matita/tests/test2.ma +++ b/helm/matita/tests/test2.ma @@ -1,8 +1,8 @@ set "baseuri" "cic:/matita/tests/test2/". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -alias symbol "and" (instance 0) = "logical and". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "and" (instance 0) = "Coq's logical and". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:\forall x:nat.x=x\land x=x. intro. split. diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma index 9a8958b21..561bd6564 100644 --- a/helm/matita/tests/test3.ma +++ b/helm/matita/tests/test3.ma @@ -1,6 +1,6 @@ set "baseuri" "cic:/matita/tests/test3/". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:\forall x.x=x. alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". exact nat. @@ -8,7 +8,7 @@ intro. reflexivity. qed. alias num (instance 0) = "natural number". -alias symbol "times" (instance 0) = "natural times". +alias symbol "times" (instance 0) = "Coq's natural times". theorem b:\forall p:nat. p * 0=0. intro. diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma index be67f3a8e..8d8cac4e3 100644 --- a/helm/matita/tests/test4.ma +++ b/helm/matita/tests/test4.ma @@ -6,7 +6,7 @@ set "baseuri" "cic:/matita/tests/test4/". *) alias num (instance 0) = "natural number". -alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:0=0. (* nota *)