X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Ftest3.ma;h=cb2cece18730d3828813b2bfe09c1f0fdace3697;hb=c0f06261e5626228e4681de9973b6412524f09a2;hp=e589c5aaa8361b84978069f14514ac901df5e852;hpb=6b8da04f526b3484dc92f61a23a8e61e63422c13;p=helm.git diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma index e589c5aaa..cb2cece18 100644 --- a/helm/matita/tests/test3.ma +++ b/helm/matita/tests/test3.ma @@ -1,7 +1,6 @@ alias symbol "eq" (instance 0) = "leibnitz's equality". theorem a:\forall x.x=x. alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -goal 5. exact nat. intro. reflexivity. @@ -12,5 +11,4 @@ alias symbol "times" (instance 0) = "natural times". theorem b:\forall p:nat. p * 0=0. intro. auto. -abort. -qed. \ No newline at end of file +qed.