From: Ferruccio Guidi Date: Wed, 25 Jun 2014 13:20:54 +0000 (+0000) Subject: pathologic @-typing removed by adding imp-introduction X-Git-Tag: make_still_working~893 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b5da1e71c94a3c3a7fe6a50e71e75367b02828df;p=helm.git pathologic @-typing removed by adding imp-introduction --- 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(b,mp"l"(a,con,x,n)):imp(a,b) b@ec:=[x:a]not(b):'prop' [n:not(a)] eci1:=[x:a]cone(not(b),mp"l"(a,con,x,n)):ec(a,b) -%suggestion by Guidi to remove @-typing -b@[a1:and(a,b)] %original line -ande2:=ande2"l"(a,b,a1):b %original line -%b@[a1:and(a,[x:a]b)] -%ande2:=b,a1)>ande2"l"(a,[x:a]b,a1):b,a1)>[x:a]b +%suggestion by Guidi to remove @-typing by adding imp-introduction +%b@[a1:and(a,b)] %original line +%ande2:=ande2"l"(a,b,a1):b %original line +b@[a1:and(a,imp(a,b))] +ande2:=ande2"l"(a,imp(a,b),a1):b %end of suggestion a@[ksi:'type'] +ite