src/HOL/Library/Zorn.thy
changeset 44890 22f665a2e91c
parent 35175 61255c81da01
child 46008 c296c75f4cf4
     1.1 --- a/src/HOL/Library/Zorn.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -480,12 +480,12 @@
     1.4          by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis
     1.5        thus ?thesis using `wf(m-Id)` `x \<notin> Field m`
     1.6          wf_subset[OF `wf ?s` Diff_subset]
     1.7 -        by (fastsimp intro!: wf_Un simp add: Un_Diff Field_def)
     1.8 +        by (fastforce intro!: wf_Un simp add: Un_Diff Field_def)
     1.9      qed
    1.10      ultimately have "Well_order ?m" by(simp add:order_on_defs)
    1.11  --{*We show that the extension is above m*}
    1.12      moreover hence "(m,?m) : I" using `Well_order m` `x \<notin> Field m`
    1.13 -      by(fastsimp simp:I_def init_seg_of_def Field_def Domain_def Range_def)
    1.14 +      by(fastforce simp:I_def init_seg_of_def Field_def Domain_def Range_def)
    1.15      ultimately
    1.16  --{*This contradicts maximality of m:*}
    1.17      have False using max `x \<notin> Field m` unfolding Field_def by blast
    1.18 @@ -501,7 +501,7 @@
    1.19      using well_ordering[where 'a = "'a"] by blast
    1.20    let ?r = "{(x,y). x:A & y:A & (x,y):r}"
    1.21    have 1: "Field ?r = A" using wo univ
    1.22 -    by(fastsimp simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
    1.23 +    by(fastforce simp: Field_def Domain_def Range_def order_on_defs refl_on_def)
    1.24    have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)"
    1.25      using `Well_order r` by(simp_all add:order_on_defs)
    1.26    have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ)