src/HOL/Lambda/ParRed.thy

 theory ParRed imports Lambda Commutation begin
 
 
 subsection {* Parallel reduction *}
 
-inductive2 par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
+inductive 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_cases2 par_beta_cases [elim!]:
+inductive_cases par_beta_cases [elim!]:
   "Var n => t"
   "Abs s => Abs t"
   "(Abs s) \<degree> t => u"
   "s \<degree> t => u"
   "Abs s => t"

 
 lemma par_beta_subset_beta: "par_beta <= beta^**"
   apply (rule predicate2I)
   apply (erule par_beta.induct)
      apply blast
-    apply (blast del: rtrancl.rtrancl_refl intro: rtrancl.rtrancl_into_rtrancl)+
+    apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+
       -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
   done
 
 
 subsection {* Misc properties of par-beta *}