From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
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(<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