--- a/src/HOL/Lambda/Lambda.thy Thu Jun 06 13:13:18 1996 +0200
+++ b/src/HOL/Lambda/Lambda.thy Thu Jun 06 14:39:44 1996 +0200
@@ -48,7 +48,7 @@
"s -> t" == "(s,t) : beta"
"s ->> t" == "(s,t) : beta^*"
-inductive "beta"
+inductive beta
intrs
beta "(Fun s) @ t -> s[t/0]"
appL "s -> t ==> s@u -> t@u"