X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fparatest.ma;h=93970a1d495e4ce2a96d66652356eb67e32449b2;hb=df7a2aa19e98dc28e7f22129275a175cead49e2d;hp=de4c4204887a77adb0b93f0158c5b184cfbea107;hpb=01b628fc79155f545b283c1d095d8a2ffe00e0a1;p=helm.git

diff --git a/helm/software/matita/tests/paratest.ma b/helm/software/matita/tests/paratest.ma
index de4c42048..93970a1d4 100644
--- a/helm/software/matita/tests/paratest.ma
+++ b/helm/software/matita/tests/paratest.ma
@@ -14,9 +14,20 @@
 
 include "nat/plus.ma".
 
+(*ntheorem boo:
+   (∀x. x = x) → 0 = 0. 
+##[ #H; nwhd in H ⊢ %; nauto by H.*)
+
+ntheorem bboo:
+  (∀x. x + 0 = x) ->
+  (∀x, y. x + S y = S (x + y)) →
+  (∀x, y. x + y = y + x) →
+  3 + 2 = 5.
+#H; #H1; #H2; nauto by H, H1. H2.
+  
 ntheorem foo:  
    ((λx.x + 0 = x) ?) → 
    ((λx,y.x + S y = S (x + y)) ? ?) →
-   ((λx,y.y + x = x + y) ? ?) →
-   ∀x. ((λz. x + x = z + S z) ?). 
-##[ #H; #H1; #H2; #x; nnormalize in H H1 H2 ⊢ %; nauto by H, H1, H2.
\ No newline at end of file
+   ((λx,y.x y = x y) ? ?) →
+   ∀x. ((λz. x + x = z + z) ?). 
+##[ #H; #H1; #H2; #x; nwhd in H H1 H2 ⊢ %; nauto by H, H1, H2.
\ No newline at end of file