X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fexamples%2Fgrundlagen%2Fgrundlagen.aut;fp=helm%2Fsoftware%2Fhelena%2Fexamples%2Fgrundlagen%2Fgrundlagen.aut;h=d4d9528e8bf876a9478664df076f59bfd50b4dfc;hb=b5da1e71c94a3c3a7fe6a50e71e75367b02828df;hp=d38532d369ee0903476d1406f88bd83b3af51f1b;hpb=f6923ff81abc829b20c6d01801fd6b98ab88cd65;p=helm.git

diff --git a/helm/software/helena/examples/grundlagen/grundlagen.aut b/helm/software/helena/examples/grundlagen/grundlagen.aut
index d38532d36..d4d9528e8 100644
--- a/helm/software/helena/examples/grundlagen/grundlagen.aut
+++ b/helm/software/helena/examples/grundlagen/grundlagen.aut
@@ -682,11 +682,11 @@ th2:=[x:a]cone(<x>b,mp"l"(a,con,x,n)):imp(a,b)
 b@ec:=[x:a]not(<x>b):'prop'
 [n:not(a)]
 eci1:=[x:a]cone(not(<x>b),mp"l"(a,con,x,n)):ec(a,b)
-%suggestion by Guidi to remove @-typing
-b@[a1:and(a,b)] %original line
-ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b %original line
-%b@[a1:and(a,[x:a]<x>b)]
-%ande2:=<ande1(a,[x:a]<x>b,a1)>ande2"l"(a,[x:a]<x>b,a1):<ande1(a,[x:a]<x>b,a1)>[x:a]<x>b
+%suggestion by Guidi to remove @-typing by adding imp-introduction
+%b@[a1:and(a,b)] %original line
+%ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b %original line
+b@[a1:and(a,imp(a,b))]
+ande2:=<ande1(a,imp(a,b),a1)>ande2"l"(a,imp(a,b),a1):<ande1(a,imp(a,b),a1)>b
 %end of suggestion
 a@[ksi:'type']
 +ite