src/HOL/ex/Dedekind_Real.thy
changeset 46905 6b1c0a80a57a
parent 45694 4a8743618257
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:40:06 2012 +0100
     1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:56:56 2012 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4  by (simp add: preal_def cut_of_rat)
     1.5  
     1.6  lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
     1.7 -  unfolding preal_def cut_def_raw by blast
     1.8 +  unfolding preal_def cut_def [abs_def] by blast
     1.9  
    1.10  lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
    1.11    apply (drule preal_nonempty)
    1.12 @@ -131,10 +131,10 @@
    1.13    done
    1.14  
    1.15  lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
    1.16 -  unfolding preal_def cut_def_raw by blast
    1.17 +  unfolding preal_def cut_def [abs_def] by blast
    1.18  
    1.19  lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
    1.20 -  unfolding preal_def cut_def_raw by blast
    1.21 +  unfolding preal_def cut_def [abs_def] by blast
    1.22  
    1.23  text{*Relaxing the final premise*}
    1.24  lemma preal_downwards_closed':
    1.25 @@ -966,7 +966,7 @@
    1.26  
    1.27  lemma mem_diff_set:
    1.28       "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
    1.29 -apply (unfold preal_def cut_def_raw)
    1.30 +apply (unfold preal_def cut_def [abs_def])
    1.31  apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
    1.32                       diff_set_lemma3 diff_set_lemma4)
    1.33  done
    1.34 @@ -1135,7 +1135,7 @@
    1.35  
    1.36  lemma preal_sup:
    1.37       "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
    1.38 -apply (unfold preal_def cut_def_raw)
    1.39 +apply (unfold preal_def cut_def [abs_def])
    1.40  apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
    1.41                       preal_sup_set_lemma3 preal_sup_set_lemma4)
    1.42  done