# HG changeset patch
# User hoelzl
# Date 1354719525 -3600
# Node ID 837e38a42d8cb3440a306c6f68054ee4dd5f1e32
# Parent  b9b967da28e9ee4e57bad0192d46388f1a202603
Remove looping rule from measurability prover

diff -r b9b967da28e9 -r 837e38a42d8c src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Dec 04 20:44:18 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Dec 05 15:58:45 2012 +0100
@@ -941,8 +941,8 @@
 qed (auto simp: e2p_def)
 
 (* FIXME: conversion in measurable prover *)
-lemma lborelD_Collect[measurable]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
-lemma lborelD[measurable]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
+lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
+lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
 
 lemma measurable_p2e[measurable]:
   "p2e \<in> measurable (\<Pi>\<^isub>M i\<in>{..<DIM('a)}. (lborel :: real measure))