+# 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']
imp:=[x:a]b:'prop'
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
-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