X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Fclearbody.ma;h=29dd2457dae94317c6561786c206d2bb07743e51;hb=d35d134356645a09eb72db6e484f3df583123af1;hp=b38de22dbd0ec3866a7d20f2127dce94f677b3cb;hpb=98f91a1c3b122ac026e38d16c9cbac50f9562f7d;p=helm.git

diff --git a/helm/matita/tests/clearbody.ma b/helm/matita/tests/clearbody.ma
index b38de22db..29dd2457d 100644
--- a/helm/matita/tests/clearbody.ma
+++ b/helm/matita/tests/clearbody.ma
@@ -19,7 +19,7 @@ alias symbol "plus" (instance 0) = "natural plus".
 
 
 theorem stupid : 
-  let x \def 0 + 1 in x + 1= x + 1.
+  let x \def 0 + 1 in x + 2 = x + 2.
   intros.
   clearbody x. 
   simplify.