diff -r 4ccb7e6be929 -r 51a80e238b29 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Wed Feb 07 17:41:11 2007 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Wed Feb 07 17:44:07 2007 +0100
@@ -14,21 +14,14 @@
 
 subsection {* Parallel reduction *}
 
-consts
-  par_beta :: "(dB \<times> dB) set"
-
-abbreviation
-  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50) where
-  "s => t == (s, t) \<in> par_beta"
+inductive2 par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
+  where
+    var [simp, intro!]: "Var n => Var n"
+  | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
+  | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
+  | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
 
-inductive par_beta
-  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 \<degree> t => s' \<degree> t'"
-    beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
-
-inductive_cases par_beta_cases [elim!]:
+inductive_cases2 par_beta_cases [elim!]:
   "Var n => t"
   "Abs s => Abs t"
   "(Abs s) \<degree> t => u"
@@ -48,18 +41,16 @@
   by (induct t) simp_all
 
 lemma beta_subset_par_beta: "beta <= par_beta"
-  apply (rule subsetI)
-  apply clarify
+  apply (rule predicate2I)
   apply (erule beta.induct)
      apply (blast intro!: par_beta_refl)+
   done
 
-lemma par_beta_subset_beta: "par_beta <= beta^*"
-  apply (rule subsetI)
-  apply clarify
+lemma par_beta_subset_beta: "par_beta <= beta^**"
+  apply (rule predicate2I)
   apply (erule par_beta.induct)
      apply blast
-    apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
+    apply (blast del: rtrancl.rtrancl_refl intro: rtrancl.rtrancl_into_rtrancl)+
       -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
   done