1) added simplification of actives w.r.t. selected

[helm.git] / helm / software / matita / tests / paratest.ma

diff --git a/helm/software/matita/tests/paratest.ma b/helm/software/matita/tests/paratest.ma
index de4c4204887a77adb0b93f0158c5b184cfbea107..68fe4cdde555e7ce9db3a560a47b8708e6abcee6 100644 (file)
--- a/helm/software/matita/tests/paratest.ma
+++ b/helm/software/matita/tests/paratest.ma
@@ -14,9 +14,13 @@
 
 include "nat/plus.ma".
 
+ntheorem boo: 
+   ((λx.x = x) ?) → 0 = 0. 
+##[ #H; nwhd in H ⊢ %; nauto by H.
+  
 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
+##[ #H; #H1; #H2; #x; nwhd in H H1 H2 ⊢ %; nauto by H, H1, H2.
\ No newline at end of file