Instantiated some rules to avoid problems with HO unification.
--- a/src/HOL/Induct/LList.thy Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/Induct/LList.thy Wed May 07 10:56:35 2008 +0200
@@ -566,7 +566,7 @@
apply (drule imageI)
apply (erule LList_equalityI, safe)
apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ f])+
apply assumption
done
@@ -574,7 +574,7 @@
apply (drule imageI)
apply (erule LList_equalityI, safe)
apply (erule llist.cases, simp_all)
-apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I, of _ _ _ "%x. x"])+
apply assumption
done
--- a/src/HOL/Inductive.thy Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/Inductive.thy Wed May 07 10:56:35 2008 +0200
@@ -112,8 +112,8 @@
and P_f: "!!S. P S ==> P(f S)"
and P_Union: "!!M. !S:M. P S ==> P(Union M)"
shows "P(lfp f)"
- using assms unfolding Sup_set_def [symmetric]
- by (rule lfp_ordinal_induct)
+ using assms unfolding Sup_set_eq [symmetric]
+ by (rule lfp_ordinal_induct [where P=P])
text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
@@ -215,7 +215,7 @@
apply (rule Un_least [THEN Un_least])
apply (rule subset_refl, assumption)
apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
-apply (rule monoD, assumption)
+apply (rule monoD [where f=f], assumption)
apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
done
--- a/src/HOL/NumberTheory/EulerFermat.thy Wed May 07 10:56:34 2008 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.thy Wed May 07 10:56:35 2008 +0200
@@ -162,7 +162,7 @@
lemma RRset_gcd [rule_format]:
"is_RRset A m ==> a \<in> A --> zgcd (a, m) = 1"
apply (unfold is_RRset_def)
- apply (rule RsetR.induct, auto)
+ apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd (a, m) = 1"], auto)
done
lemma RsetR_zmult_mono:
@@ -219,7 +219,7 @@
"1 < m ==>
is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b"
apply (unfold is_RRset_def)
- apply (rule RsetR.induct)
+ apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"])
apply (auto simp add: zcong_sym)
done