diff -r 647e6c84323c -r 2c3dee321b4b src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Fri Sep 28 20:09:10 2001 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Fri Sep 28 21:45:11 2001 +0200
@@ -23,11 +23,11 @@
   "s => t" == "(s, t) \<in> par_beta"
 
 inductive par_beta
-  intros [simp, intro!]
-    var: "Var n => Var n"
-    abs: "s => t ==> Abs s => Abs t"
-    app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
-    beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
+  intros
+    var [simp, intro!]: "Var n => Var n"
+    abs [simp, intro!]: "s => t ==> Abs s => Abs t"
+    app [simp, intro!]: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
+    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
 
 inductive_cases par_beta_cases [elim!]:
   "Var n => t"
@@ -130,4 +130,4 @@
     par_beta_subset_beta beta_subset_par_beta)+
   done
 
-end
\ No newline at end of file
+end