fixed some macros, added test_abort.ma

[helm.git] / helm / matita / tests / test3.ma

diff --git a/helm/matita/tests/test3.ma b/helm/matita/tests/test3.ma
index c4aafaf3c6f64390c0300878d645bae933c0ceb1..e589c5aaa8361b84978069f14514ac901df5e852 100644 (file)
--- 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