X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Ftest3.ma;h=e589c5aaa8361b84978069f14514ac901df5e852;hb=6b8da04f526b3484dc92f61a23a8e61e63422c13;hp=c4aafaf3c6f64390c0300878d645bae933c0ceb1;hpb=2007173e83a5001053c2946b59d6827cc080f1c4;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