author noschinl Thu Feb 20 15:14:37 2014 +0100 (2014-02-20) changeset 55604 42e4e8c2e8dc parent 55603 48596c45bf7f child 55605 b1b363e81c87 child 55606 75a639ddc05f
less flex-flex pairs
 src/HOL/BNF_Cardinal_Arithmetic.thy file | annotate | diff | revisions src/HOL/Inductive.thy file | annotate | diff | revisions src/HOL/Lifting.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Thu Feb 20 13:53:26 2014 +0100
1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Thu Feb 20 15:14:37 2014 +0100
1.3 @@ -400,7 +400,8 @@
1.4    proof (cases "Field p2 = {}")
1.5      case True
1.6      with n have "Field r2 = {}" .
1.7 -    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def by (auto intro: card_of_ordLeqI)
1.8 +    hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def
1.9 +      by (auto intro: card_of_ordLeqI[where f="\<lambda>_ _. undefined"])
1.10      thus ?thesis using `p1 ^c p2 \<le>o cone` ordLeq_transitive by auto
1.11    next
1.12      case False with True have "|Field (p1 ^c p2)| =o czero"
```
```     2.1 --- a/src/HOL/Inductive.thy	Thu Feb 20 13:53:26 2014 +0100
2.2 +++ b/src/HOL/Inductive.thy	Thu Feb 20 15:14:37 2014 +0100
2.3 @@ -177,12 +177,13 @@
2.4
2.5  text{*strong version, thanks to Coen and Frost*}
2.6  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
2.7 -  by (blast intro: weak_coinduct [OF _ coinduct_lemma])
2.8 +  by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
2.9
2.10  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
2.11    apply (rule order_trans)
2.12    apply (rule sup_ge1)
2.13 -  apply (erule gfp_upperbound [OF coinduct_lemma])
2.14 +  apply (rule gfp_upperbound)
2.15 +  apply (erule coinduct_lemma)
2.16    apply assumption
2.17    done
2.18
```
```     3.1 --- a/src/HOL/Lifting.thy	Thu Feb 20 13:53:26 2014 +0100
3.2 +++ b/src/HOL/Lifting.thy	Thu Feb 20 15:14:37 2014 +0100
3.3 @@ -455,13 +455,13 @@
3.4    assumes "left_unique T"
3.5    assumes "R \<le> op="
3.6    shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
3.7 -using assms unfolding left_unique_def by fast
3.8 +using assms unfolding left_unique_def by blast
3.9
3.10  lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
3.11  unfolding left_total_def OO_def by fast
3.12
3.13  lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
3.14 -unfolding left_unique_def OO_def by fast
3.15 +unfolding left_unique_def OO_def by blast
3.16
3.17  lemma invariant_le_eq:
3.18    "invariant P \<le> op=" unfolding invariant_def by blast
```