X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2Fgrundlagen.aut;h=4a856c2454454abafef49c36af35960d94636082;hb=a872dba2b03e27967d5b9b51e950e85967340e52;hp=186ebdbcc79eaecee9c05ade652d9c60ee73e74f;hpb=ae63e62aaf5659fe6b0e48cc4a4bdcf7b57318ad;p=helm.git

diff --git a/helm/software/lambda-delta/automath/grundlagen.aut b/helm/software/lambda-delta/automath/grundlagen.aut
index 186ebdbcc..4a856c245 100644
--- a/helm/software/lambda-delta/automath/grundlagen.aut
+++ b/helm/software/lambda-delta/automath/grundlagen.aut
@@ -5,17 +5,9 @@
 
 +l
 @[a:'prop'][b:'prop']
-%modification by Guidi to avoid prop inclusion
-%imp:=[x:a]b:'prop' %original line
-imp:='prim':'prop'
-%end of modification
+imp:=[x:a]b:'prop'
 [a1:a][i:imp(a,b)]
-%modification by Guidi to avoid prop inclusion
-%mp:=<a1>i:b %original line
-mp:='prim':b
-b@[f:[x:a]b] % we define modus tollens
-mt:='prim':imp(a,b)
-%end of modification
+mp:=<a1>i:b
 a@refimp:=[x:a]x:imp(a,a)
 b@[c:'prop'][i:imp(a,b)][j:imp(b,c)]
 trimp:=[x:a]<<x>i>j:imp(a,c)
@@ -23,7 +15,7 @@ trimp:=[x:a]<<x>i>j:imp(a,c)
 a@not:=imp(con):'prop'
 wel:=not(not(a)):'prop'
 [a1:a]
-weli:=[x:not(a)]<a1>x:wel(a) %original line
+weli:=[x:not(a)]<a1>x:wel(a)
 a@[w:wel(a)]
 et:='prim':a
 a@[c1:con]
@@ -233,26 +225,17 @@ i@[o:orec(c,a)]
 thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b)
 -iff
 @[sigma:'type'][p:[x:sigma]'prop']
-%modification by Guidi to remove prop inclusion
+%suggestion by van Daalen to remove the first eta-reduction
 %all:=p:'prop' %original line
-%all:=[x:sigma]<x>p:'prop' %suggestion by van Daalen to remove eta-reduction 
-all:='prim':'prop'
-%end of modification
+all:=[x:sigma]<x>p:'prop'
+%end of suggestion
 [a1:all(sigma,p)][s:sigma]
-%modification by Guidi to remove prop inclusion
-%alle:=<s>a1:<s>p %original line
-alle:='prim':<s>p
-p@[f:[s:sigma]<s>p] % we define modus tollens
-alli:='prim':all(sigma,p)
-%end of modification
+alle:=<s>a1:<s>p
 +all
 p@[s:sigma][n:not(<s>p)]
 th1:=[x:all(sigma,p)]<<s>x>n:not(all(sigma,p))
 -all
 p@non:=[x:sigma]not(<x>p):[x:sigma]'prop'
-%modification by Guidi to remove prop inclusion
-p@lppc0:='prim':'prop'
-%end of modification
 some:=not(non(p)):'prop'
 [s:sigma][sp:<s>p]
 somei:=th1".all"(non(p),s,weli(<s>p,sp)):some(sigma,p)