X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Ftest3.ma;h=e589c5aaa8361b84978069f14514ac901df5e852;hb=e6708c10ad615233628900902101216cc2f5baf5;hp=c4aafaf3c6f64390c0300878d645bae933c0ceb1;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma
index c4aafaf3c..e589c5aaa 100644
--- a/helm/matita/tests/test3.ma
+++ b/helm/matita/tests/test3.ma
@@ -5,4 +5,12 @@ goal 5.
 exact nat.
 intro.
 reflexivity.
+qed.
+alias num (instance 0) = "natural number".
+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