--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Thu Feb 20 13:53:26 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Thu Feb 20 15:14:37 2014 +0100
@@ -400,7 +400,8 @@
proof (cases "Field p2 = {}")
case True
with n have "Field r2 = {}" .
- hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
+ hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def
+ by (auto intro: card_of_ordLeqI[where f="\<lambda>_ _. undefined"])
thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
next
case False with True have "|Field (p1 ^c p2)| =o czero"
--- a/src/HOL/Inductive.thy Thu Feb 20 13:53:26 2014 +0100
+++ b/src/HOL/Inductive.thy Thu Feb 20 15:14:37 2014 +0100
@@ -177,12 +177,13 @@
text{*strong version, thanks to Coen and Frost*}
lemma coinduct_set: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
- by (blast intro: weak_coinduct [OF _ coinduct_lemma])
+ by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
apply (rule order_trans)
apply (rule sup_ge1)
- apply (erule gfp_upperbound [OF coinduct_lemma])
+ apply (rule gfp_upperbound)
+ apply (erule coinduct_lemma)
apply assumption
done
--- a/src/HOL/Lifting.thy Thu Feb 20 13:53:26 2014 +0100
+++ b/src/HOL/Lifting.thy Thu Feb 20 15:14:37 2014 +0100
@@ -455,13 +455,13 @@
assumes "left_unique T"
assumes "R \<le> op="
shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
-using assms unfolding left_unique_def by fast
+using assms unfolding left_unique_def by blast
lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
unfolding left_total_def OO_def by fast
lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
-unfolding left_unique_def OO_def by fast
+unfolding left_unique_def OO_def by blast
lemma invariant_le_eq:
"invariant P \<le> op=" unfolding invariant_def by blast