author wenzelm Tue Mar 13 16:56:56 2012 +0100 (2012-03-13 ago) changeset 46905 6b1c0a80a57a parent 46904 f30e941b4512 child 46906 3c1787d46935
prefer abs_def over def_raw;
```     1.1 --- a/src/HOL/Import/HOL_Light/Compatibility.thy	Tue Mar 13 16:40:06 2012 +0100
1.2 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy	Tue Mar 13 16:56:56 2012 +0100
1.3 @@ -272,7 +272,7 @@
1.4
1.5  lemma DEF_DISJOINT:
1.6    "DISJOINT = (%u ua. u \<inter> ua = {})"
1.7 -  by (auto simp add: DISJOINT_def_raw)
1.8 +  by (auto simp add: DISJOINT_def [abs_def])
1.9
1.10  lemma DEF_DIFF:
1.11    "op - = (\<lambda>u ua. {ub. \<exists>x. (x \<in> u \<and> x \<notin> ua) \<and> ub = x})"
1.12 @@ -282,7 +282,7 @@
1.13
1.14  lemma DEF_DELETE:
1.15    "DELETE = (\<lambda>u ua. {ub. \<exists>y. (y \<in> u \<and> y \<noteq> ua) \<and> ub = y})"
1.16 -  by (auto simp add: DELETE_def_raw)
1.17 +  by (auto simp add: DELETE_def [abs_def])
1.18
1.19  lemma COND_DEF:
1.20    "(if b then t else f) = (SOME x. (b = True \<longrightarrow> x = t) \<and> (b = False \<longrightarrow> x = f))"
1.21 @@ -344,7 +344,7 @@
1.22  definition [import_rew,simp]: "INFINITE S \<longleftrightarrow> \<not> finite S"
1.23
1.24  lemma DEF_INFINITE: "INFINITE = (\<lambda>u. \<not>finite u)"
1.25 -  by (simp add: INFINITE_def_raw)
1.26 +  by (simp add: INFINITE_def [abs_def])
1.27
1.28  end
1.29
```
```     2.1 --- a/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 13 16:40:06 2012 +0100
2.2 +++ b/src/HOL/Import/HOL_Light/HOLLightInt.thy	Tue Mar 13 16:56:56 2012 +0100
2.3 @@ -90,7 +90,7 @@
2.4
2.5  lemma int_mod_def':
2.6    "int_mod = (\<lambda>u ua ub. (u dvd (ua - ub)))"
2.7 -  by (simp add: int_mod_def_raw)
2.8 +  by (simp add: int_mod_def [abs_def])
2.9
2.10  lemma int_congruent:
2.11    "\<forall>x xa xb. int_mod xb x xa = (\<exists>d. x - xa = xb * d)"
```
```     3.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Mar 13 16:40:06 2012 +0100
3.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Tue Mar 13 16:56:56 2012 +0100
3.3 @@ -7,9 +7,9 @@
3.4  declare HOL.if_bool_eq_disj[code_pred_inline]
3.5
3.6  declare bool_diff_def[code_pred_inline]
3.7 -declare inf_bool_def_raw[code_pred_inline]
3.8 -declare less_bool_def_raw[code_pred_inline]
3.9 -declare le_bool_def_raw[code_pred_inline]
3.10 +declare inf_bool_def[abs_def, code_pred_inline]
3.11 +declare less_bool_def[abs_def, code_pred_inline]
3.12 +declare le_bool_def[abs_def, code_pred_inline]
3.13
3.14  lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
3.15  by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 13 16:40:06 2012 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 13 16:56:56 2012 +0100
4.3 @@ -2762,12 +2762,24 @@
4.4
4.5  lemma negligible:  "negligible s \<longleftrightarrow> (\<forall>t::('a::ordered_euclidean_space) set. ((indicator s::'a\<Rightarrow>real) has_integral 0) t)"
4.6    apply safe defer apply(subst negligible_def)
4.7 -proof- fix t::"'a set" assume as:"negligible s"
4.8 -  have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)" by(rule ext,auto)
4.9 -  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t" apply(subst has_integral_alt)
4.10 -    apply(cases,subst if_P,assumption) unfolding if_not_P apply(safe,rule as[unfolded negligible_def,rule_format])
4.11 -    apply(rule_tac x=1 in exI) apply(safe,rule zero_less_one) apply(rule_tac x=0 in exI)
4.12 -    using negligible_subset[OF as,of "s \<inter> t"] unfolding negligible_def indicator_def_raw unfolding * by auto qed auto
4.13 +proof -
4.14 +  fix t::"'a set" assume as:"negligible s"
4.15 +  have *:"(\<lambda>x. if x \<in> s \<inter> t then 1 else 0) = (\<lambda>x. if x\<in>t then if x\<in>s then 1 else 0 else 0)"
4.16 +    by auto
4.17 +  show "((indicator s::'a\<Rightarrow>real) has_integral 0) t"
4.18 +    apply(subst has_integral_alt)
4.19 +    apply(cases,subst if_P,assumption)
4.20 +    unfolding if_not_P
4.21 +    apply(safe,rule as[unfolded negligible_def,rule_format])
4.22 +    apply(rule_tac x=1 in exI)
4.23 +    apply(safe,rule zero_less_one)
4.24 +    apply(rule_tac x=0 in exI)
4.25 +    using negligible_subset[OF as,of "s \<inter> t"]
4.26 +    unfolding negligible_def indicator_def [abs_def]
4.27 +    unfolding *
4.28 +    apply auto
4.29 +    done
4.30 +qed auto
4.31
4.32  subsection {* Finite case of the spike theorem is quite commonly needed. *}
4.33
```
```     5.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Mar 13 16:40:06 2012 +0100
5.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Tue Mar 13 16:56:56 2012 +0100
5.3 @@ -149,7 +149,7 @@
5.4
5.5  lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
5.6  nitpick [expect = none]
5.7 -by (rule Zero_nat_def_raw)
5.8 +by (rule Zero_nat_def [abs_def])
5.9
5.10  lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
5.11  nitpick [expect = none]
```
```     6.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Mar 13 16:40:06 2012 +0100
6.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Tue Mar 13 16:56:56 2012 +0100
6.3 @@ -32,7 +32,7 @@
6.4  lemma [code_pred_def]:
6.5    "cardsp [] g k = False"
6.6    "cardsp (e # s) g k = (let C = cardsp s g in case e of Check_in g' r c => if g' = g then k = c \<or> C k else C k | _ => C k)"
6.7 -unfolding cardsp_def_raw cards.simps by (auto simp add: Let_def split: event.split)
6.8 +unfolding cardsp_def [abs_def] cards.simps by (auto simp add: Let_def split: event.split)
6.9
6.10  definition
6.11    "isinp evs r g = (g \<in> isin evs r)"
6.12 @@ -44,7 +44,7 @@
6.13     in case e of Check_in g' r c => G g
6.14      | Enter g' r' c => if r' = r then g = g' \<or> G g else G g
6.15      | Exit g' r' => if r' = r then ((g \<noteq> g') \<and> G g) else G g)"
6.16 -unfolding isinp_def_raw isin.simps by (auto simp add: Let_def split: event.split)
6.17 +unfolding isinp_def [abs_def] isin.simps by (auto simp add: Let_def split: event.split)
6.18
6.19  declare hotel.simps(1)[code_pred_def]
6.20  lemma [code_pred_def]:
```
```     7.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 13 16:40:06 2012 +0100
7.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 13 16:56:56 2012 +0100
7.3 @@ -90,7 +90,7 @@
7.4  lemma (in sigma_algebra) borel_measurable_indicator[simp, intro!]:
7.5    assumes A: "A \<in> sets M"
7.6    shows "indicator A \<in> borel_measurable M"
7.7 -  unfolding indicator_def_raw using A
7.8 +  unfolding indicator_def [abs_def] using A
7.9    by (auto intro!: measurable_If_set borel_measurable_const)
7.10
7.11  lemma (in sigma_algebra) borel_measurable_indicator_iff:
7.12 @@ -101,7 +101,7 @@
7.13    then have "?I -` {1} \<inter> space M \<in> sets M"
7.14      unfolding measurable_def by auto
7.15    also have "?I -` {1} \<inter> space M = A \<inter> space M"
7.16 -    unfolding indicator_def_raw by auto
7.17 +    unfolding indicator_def [abs_def] by auto
7.18    finally show "A \<inter> space M \<in> sets M" .
7.19  next
7.20    assume "A \<inter> space M \<in> sets M"
```
```     8.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
8.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
8.3 @@ -706,7 +706,7 @@
8.4    have "\<And>A. measure (Pi\<^isub>M {} M) (Pi\<^isub>E {} A) = 1"
8.5      using assms by (subst measure_times) auto
8.6    then show ?thesis
8.7 -    unfolding positive_integral_def simple_function_def simple_integral_def_raw
8.8 +    unfolding positive_integral_def simple_function_def simple_integral_def [abs_def]
8.9    proof (simp add: P_empty, intro antisym)
8.10      show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
8.11        by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
```
```     9.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
9.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
9.3 @@ -874,7 +874,7 @@
9.4        by (simp add: sets_sigma product_algebra_generator_def product_algebra_def)
9.5      also have "\<dots> = sigma_sets (space (Pi\<^isub>M I M)) (emb I J ` Pi\<^isub>E J ` (\<Pi> i \<in> J. sets (M i)))"
9.6        using J M.sets_into_space
9.7 -      by (auto simp: emb_def_raw intro!: sigma_sets_vimage[symmetric]) blast
9.8 +      by (auto simp: emb_def [abs_def] intro!: sigma_sets_vimage[symmetric]) blast
9.9      also have "\<dots> \<subseteq> sigma_sets (space (Pi\<^isub>M I M)) ?M"
9.10        using J by (intro sigma_sets_mono') auto
9.11      finally show "emb I J ` sets (Pi\<^isub>M J M) \<subseteq> sigma_sets ?O ?M"
```
```    10.1 --- a/src/HOL/Probability/Information.thy	Tue Mar 13 16:40:06 2012 +0100
10.2 +++ b/src/HOL/Probability/Information.thy	Tue Mar 13 16:56:56 2012 +0100
10.3 @@ -823,7 +823,7 @@
10.4    interpret S: prob_space "S\<lparr> measure := ereal\<circ>distribution X \<rparr>"
10.5      using distribution_prob_space[OF X] .
10.6    from A show "S.\<mu>' A = distribution X A"
10.7 -    unfolding S.\<mu>'_def by (simp add: distribution_def_raw \<mu>'_def)
10.8 +    unfolding S.\<mu>'_def by (simp add: distribution_def [abs_def] \<mu>'_def)
10.9  qed
10.10
10.11  lemma (in information_space) entropy_uniform_max:
```
```    11.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 13 16:40:06 2012 +0100
11.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 13 16:56:56 2012 +0100
11.3 @@ -247,7 +247,7 @@
11.4    hence "finite ?S" by (rule finite_subset) simp
11.5    moreover have "- A \<inter> space M = space M - A" by auto
11.6    ultimately show ?thesis unfolding simple_function_def
11.7 -    using assms by (auto simp: indicator_def_raw)
11.8 +    using assms by (auto simp: indicator_def [abs_def])
11.9  qed
11.10
11.11  lemma (in sigma_algebra) simple_function_Pair[intro, simp]:
11.12 @@ -821,7 +821,7 @@
11.13  lemma (in measure_space) simple_integral_subalgebra:
11.14    assumes N: "measure_space N" and [simp]: "space N = space M" "measure N = measure M"
11.15    shows "integral\<^isup>S N = integral\<^isup>S M"
11.16 -  unfolding simple_integral_def_raw by simp
11.17 +  unfolding simple_integral_def [abs_def] by simp
11.18
11.19  lemma (in measure_space) simple_integral_vimage:
11.20    assumes T: "sigma_algebra M'" "T \<in> measure_preserving M M'"
11.21 @@ -1482,7 +1482,7 @@
11.22    have borel[simp]:
11.23      "borel_measurable M' = borel_measurable M"
11.24      "simple_function M' = simple_function M"
11.25 -    unfolding measurable_def simple_function_def_raw by (auto simp: M')
11.26 +    unfolding measurable_def simple_function_def [abs_def] by (auto simp: M')
11.27    from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess G . note G = this
11.28    note G' = borel_measurable_simple_function[OF this(1)] simple_functionD[OF G(1)]
11.29    note G'(2)[simp]
```
```    12.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
12.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
12.3 @@ -48,7 +48,7 @@
12.4  qed
12.5
12.6  lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
12.7 -  unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
12.8 +  unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
12.9
12.10  subsection {* Lebesgue measure *}
12.11
12.12 @@ -95,7 +95,7 @@
12.13      using A by (auto intro!: integrable_sub dest: lebesgueD simp: cube_def)
12.14  next
12.15    fix n show "(indicator {} :: _\<Rightarrow>real) integrable_on cube n"
12.16 -    by (auto simp: cube_def indicator_def_raw)
12.17 +    by (auto simp: cube_def indicator_def [abs_def])
12.18  next
12.19    fix A :: "nat \<Rightarrow> 'a set" and n ::nat assume "range A \<subseteq> sets lebesgue"
12.20    then have A: "\<And>i. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
12.21 @@ -193,7 +193,7 @@
12.22    have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
12.23      unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
12.24    also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
12.25 -    unfolding indicator_def_raw has_integral_restrict_univ ..
12.26 +    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
12.27    finally show ?thesis
12.28      using has_integral_const[of "1::real" "?N" "?P"] by simp
12.29  qed
12.30 @@ -437,9 +437,9 @@
12.31    shows lmeasure_atLeastAtMost[simp]: "lebesgue.\<mu> {a..b} = ereal (content {a..b})"
12.32  proof -
12.33    have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
12.34 -    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def_raw)
12.35 +    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def])
12.36    from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
12.37 -    by (simp add: indicator_def_raw)
12.38 +    by (simp add: indicator_def [abs_def])
12.39  qed
12.40
12.41  lemma atLeastAtMost_singleton_euclidean[simp]:
12.42 @@ -504,7 +504,7 @@
12.43    and sets_lborel[simp]: "sets lborel = sets borel"
12.44    and measure_lborel[simp]: "measure lborel = lebesgue.\<mu>"
12.45    and measurable_lborel[simp]: "measurable lborel = measurable borel"
12.46 -  by (simp_all add: measurable_def_raw lborel_def)
12.47 +  by (simp_all add: measurable_def [abs_def] lborel_def)
12.48
12.49  interpretation lborel: measure_space "lborel :: ('a::ordered_euclidean_space) measure_space"
12.50    where "space lborel = UNIV"
12.51 @@ -871,7 +871,7 @@
12.52
12.53    let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
12.54    show "Int_stable ?E" using Int_stable_cuboids .
12.55 -  show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
12.56 +  show "range cube \<subseteq> sets ?E" unfolding cube_def [abs_def] by auto
12.57    show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
12.58    { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
12.59    then show "(\<Union>i. cube i) = space ?E" by auto
12.60 @@ -1001,7 +1001,7 @@
12.61      then show "(\<Union>i. cube i) = space ?E" by auto
12.62      show "incseq cube" by (intro incseq_SucI cube_subset_Suc)
12.63      show "range cube \<subseteq> sets ?E"
12.64 -      unfolding cube_def_raw by auto
12.65 +      unfolding cube_def [abs_def] by auto
12.66      show "\<And>i. measure lebesgue (cube i) \<noteq> \<infinity>"
12.68      show "measure_space lborel" by default
```
```    13.1 --- a/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
13.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
13.3 @@ -260,7 +260,7 @@
13.4  proof (rule prob_space_vimage)
13.5    show "X \<in> measure_preserving M ?S"
13.6      using X
13.7 -    unfolding measure_preserving_def distribution_def_raw
13.8 +    unfolding measure_preserving_def distribution_def [abs_def]
13.9      by (auto simp: finite_measure_eq measurable_sets)
13.10    show "sigma_algebra ?S" using X by simp
13.11  qed
```
```    14.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Mar 13 16:40:06 2012 +0100
14.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Mar 13 16:56:56 2012 +0100
14.3 @@ -132,7 +132,7 @@
14.4    have *: "{xs. length xs = n} \<noteq> {}"
14.5      by (auto intro!: exI[of _ "replicate n undefined"])
14.6    show ?thesis
14.7 -    unfolding payer_def_raw dc_crypto fst_image_times if_not_P[OF *] ..
14.8 +    unfolding payer_def [abs_def] dc_crypto fst_image_times if_not_P[OF *] ..
14.9  qed
14.10
14.11  lemma card_payer_and_inversion:
14.12 @@ -310,7 +310,7 @@
14.13    let ?sets = "{?set i | i. i < n}"
14.14
14.15    have [simp]: "length xs = n" using assms
14.16 -    by (auto simp: dc_crypto inversion_def_raw)
14.17 +    by (auto simp: dc_crypto inversion_def [abs_def])
14.18
14.19    have "{dc \<in> dc_crypto. inversion dc = xs} = (\<Union> i < n. ?set i)"
14.20      unfolding dc_crypto payer_def by auto
14.21 @@ -462,7 +462,7 @@
14.22            {dc \<in> dc_crypto. payer dc = Some (the z) \<and> inversion dc = x}"
14.23          by (auto simp add: payer_def)
14.24        moreover from x z obtain i where "z = Some i" and "i < n" by auto
14.25 -      moreover from x have "length x = n" by (auto simp: inversion_def_raw dc_crypto)
14.26 +      moreover from x have "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
14.27        ultimately
14.28        have "?dIP {(x, z)} = 2 / (real n * 2^n)" using x
14.29          by (auto simp add: card_dc_crypto card_payer_and_inversion distribution_def)
14.30 @@ -490,7 +490,7 @@
14.31        unfolding neg_equal_iff_equal
14.32      proof (rule setsum_cong[OF refl])
14.33        fix x assume x_inv: "x \<in> inversion ` dc_crypto"
14.34 -      hence "length x = n" by (auto simp: inversion_def_raw dc_crypto)
14.35 +      hence "length x = n" by (auto simp: inversion_def [abs_def] dc_crypto)
14.36        moreover have "inversion -` {x} \<inter> dc_crypto = {dc \<in> dc_crypto. inversion dc = x}" by auto
14.37        ultimately have "?dI {x} = 2 / 2^n" using `0 < n`
14.38          by (auto simp: card_inversion[OF x_inv] card_dc_crypto distribution_def)
```
```    15.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:40:06 2012 +0100
15.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Mar 13 16:56:56 2012 +0100
15.3 @@ -115,7 +115,7 @@
15.4  by (simp add: preal_def cut_of_rat)
15.5
15.6  lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
15.7 -  unfolding preal_def cut_def_raw by blast
15.8 +  unfolding preal_def cut_def [abs_def] by blast
15.9
15.10  lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
15.11    apply (drule preal_nonempty)
15.12 @@ -131,10 +131,10 @@
15.13    done
15.14
15.15  lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
15.16 -  unfolding preal_def cut_def_raw by blast
15.17 +  unfolding preal_def cut_def [abs_def] by blast
15.18
15.19  lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
15.20 -  unfolding preal_def cut_def_raw by blast
15.21 +  unfolding preal_def cut_def [abs_def] by blast
15.22
15.23  text{*Relaxing the final premise*}
15.24  lemma preal_downwards_closed':
15.25 @@ -966,7 +966,7 @@
15.26
15.27  lemma mem_diff_set:
15.28       "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
15.29 -apply (unfold preal_def cut_def_raw)
15.30 +apply (unfold preal_def cut_def [abs_def])
15.31  apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
15.32                       diff_set_lemma3 diff_set_lemma4)
15.33  done
15.34 @@ -1135,7 +1135,7 @@
15.35
15.36  lemma preal_sup:
15.37       "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
15.38 -apply (unfold preal_def cut_def_raw)
15.39 +apply (unfold preal_def cut_def [abs_def])
15.40  apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
15.41                       preal_sup_set_lemma3 preal_sup_set_lemma4)
15.42  done
```