# HG changeset patch
# User hoelzl
# Date 1301671256 -7200
# Node ID 8df8e5cc31196c2345d61038be8b7a98d8e63474
# Parent  aded341192137a6c7cf1936d9191b9a0bb1fe9d6
remove unnecessary prob_preserving

diff -r aded34119213 -r 8df8e5cc3119 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Fri Apr 01 17:20:33 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Apr 01 17:20:56 2011 +0200
@@ -36,7 +36,6 @@
 
 abbreviation (in prob_space) "events \<equiv> sets M"
 abbreviation (in prob_space) "prob \<equiv> \<mu>'"
-abbreviation (in prob_space) "prob_preserving \<equiv> measure_preserving"
 abbreviation (in prob_space) "random_variable M' X \<equiv> sigma_algebra M' \<and> X \<in> measurable M M'"
 abbreviation (in prob_space) "expectation \<equiv> integral\<^isup>L M"