lambda-delta: we added the support for position indexes in global references

[helm.git] / helm / software / lambda-delta / automath / grundlagen.aut

diff --git a/helm/software/lambda-delta/automath/grundlagen.aut b/helm/software/lambda-delta/automath/grundlagen.aut
index 34e5493abf1449c6d62c37d00f3d5e7f5c0c2773..4a856c2454454abafef49c36af35960d94636082 100644 (file)
--- a/helm/software/lambda-delta/automath/grundlagen.aut
+++ b/helm/software/lambda-delta/automath/grundlagen.aut
@@ -1,6 +1,7 @@
 # Landau's "Grundlagen der Analysis", formal specification in AUTOMATH
 # Copyright (C) 1977, L.S. van Benthem Jutting
 #               1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
+#               2008, revised by F. Guidi to remove the eta-reductions
 
 +l
 @[a:'prop'][b:'prop']
@@ -224,7 +225,10 @@ 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']
-all:=p:'prop'
+%suggestion by van Daalen to remove the first eta-reduction
+%all:=p:'prop' %original line
+all:=[x:sigma]<x>p:'prop'
+%end of suggestion
 [a1:all(sigma,p)][s:sigma]
 alle:=<s>a1:<s>p
 +all
@@ -662,7 +666,10 @@ th6:=th1"e.bij"(sigma,sigma,tau,wissel(s0,t0),f,th3(s0,t0),b):bijective(changef)
 -e
 +r
 a@[b:[x:a]'prop']
-imp:=b:'prop'
+%suggestion by van Daalen to remove the second eta-reduction
+%imp:=b:'prop' %original line
+imp:=[x:a]<x>b:'prop'
+%end of suggestion
 [a1:a][i:imp(a,b)]
 mp:=<a1>i:<a1>b
 +imp