--- a/src/HOL/NumberTheory/BijectionRel.thy Thu Dec 08 12:50:03 2005 +0100
+++ b/src/HOL/NumberTheory/BijectionRel.thy Thu Dec 08 12:50:04 2005 +0100
@@ -63,19 +63,16 @@
done
lemma aux_induct:
- "finite F ==> F \<subseteq> A ==> P {} ==>
- (!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F))
- ==> P F"
-proof -
- case rule_context
- assume major: "finite F"
+ assumes major: "finite F"
and subs: "F \<subseteq> A"
- show ?thesis
- apply (rule subs [THEN rev_mp])
- apply (rule major [THEN finite_induct])
- apply (blast intro: rule_context)+
- done
-qed
+ and cases: "P {}"
+ "!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
+ shows "P F"
+ using major subs
+ apply (induct set: Finites)
+ apply (blast intro: cases)+
+ done
+
lemma inj_func_bijR_aux1:
"A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"