--- a/src/HOL/Lambda/Lambda.thy Fri Sep 28 20:09:10 2001 +0200
+++ b/src/HOL/Lambda/Lambda.thy Fri Sep 28 21:45:11 2001 +0200
@@ -64,11 +64,11 @@
"s ->> t" == "(s, t) \<in> beta^*"
inductive beta
- intros [simp, intro!]
- beta: "Abs s $ t -> s[t/0]"
- appL: "s -> t ==> s $ u -> t $ u"
- appR: "s -> t ==> u $ s -> u $ t"
- abs: "s -> t ==> Abs s -> Abs t"
+ intros
+ beta [simp, intro!]: "Abs s $ t -> s[t/0]"
+ appL [simp, intro!]: "s -> t ==> s $ u -> t $ u"
+ appR [simp, intro!]: "s -> t ==> u $ s -> u $ t"
+ abs [simp, intro!]: "s -> t ==> Abs s -> Abs t"
inductive_cases beta_cases [elim!]:
"Var i -> t"
@@ -203,4 +203,4 @@
apply (simp add: rtrancl_beta_Abs)
done
-end
\ No newline at end of file
+end