src/ZF/Constructible/Normal.thy

 
 lemma Normal_imp_mono: "[| i<j; Normal(F) |] ==> F(i) < F(j)"
 by (simp add: Normal_def mono_Ord_def)
 
 lemma Normal_increasing: "[| Ord(i); Normal(F) |] ==> i\<le>F(i)"
-apply (induct i rule: trans_induct3_rule)
+apply (induct i rule: trans_induct3)
   apply (simp add: subset_imp_le)
  apply (subgoal_tac "F(x) < F(succ(x))")
   apply (force intro: lt_trans1)
  apply (simp add: Normal_def mono_Ord_def)
 apply (subgoal_tac "(\<Union>y<x. y) \<le> (\<Union>y<x. F(y))")

     "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) \<union> succ(r))"
 
 
 lemma Ord_normalize [simp, intro]:
      "[| Ord(a); !!x. Ord(x) ==> Ord(F(x)) |] ==> Ord(normalize(F, a))"
-apply (induct a rule: trans_induct3_rule)
+apply (induct a rule: trans_induct3)
 apply (simp_all add: ltD def_transrec2 [OF normalize_def])
 done
 
 lemma normalize_lemma [rule_format]:
      "[| Ord(b); !!x. Ord(x) ==> Ord(F(x)) |]