| changeset 6307 | fdf236c98914 |
| parent 5184 | 9b8547a9496a |
| child 9102 | c7ba07e3bbe8 |
--- a/src/HOL/Lambda/Eta.thy Mon Mar 08 13:49:14 1999 +0100 +++ b/src/HOL/Lambda/Eta.thy Mon Mar 08 13:49:53 1999 +0100 @@ -22,7 +22,7 @@ primrec "free (Var j) i = (j=i)" "free (s $ t) i = (free s i | free t i)" - "free (Abs s) i = free s (Suc i)" + "free (Abs s) i = free s (i+1)" inductive eta intrs