summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Borel_Space.thy

changeset 46884 | 154dc6ec0041 |

parent 46731 | 5302e932d1e5 |

child 46905 | 6b1c0a80a57a |

1.1 --- a/src/HOL/Probability/Borel_Space.thy Mon Mar 12 15:12:22 2012 +0100 1.2 +++ b/src/HOL/Probability/Borel_Space.thy Mon Mar 12 21:41:11 2012 +0100 1.3 @@ -1417,7 +1417,7 @@ 1.4 proof 1.5 fix a 1.6 have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})" 1.7 - by (auto simp: less_SUP_iff SUP_apply) 1.8 + by (auto simp: less_SUP_iff) 1.9 then show "?sup -` {a<..} \<inter> space M \<in> sets M" 1.10 using assms by auto 1.11 qed 1.12 @@ -1430,7 +1430,7 @@ 1.13 proof 1.14 fix a 1.15 have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})" 1.16 - by (auto simp: INF_less_iff INF_apply) 1.17 + by (auto simp: INF_less_iff) 1.18 then show "?inf -` {..<a} \<inter> space M \<in> sets M" 1.19 using assms by auto 1.20 qed