--- a/src/HOL/Probability/Probability_Measure.thy Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Oct 18 14:20:09 2024 +0200
@@ -249,10 +249,8 @@
syntax
"_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'((/_ in _./ _)'))\<close>)
-
syntax_consts
"_prob" == measure
-
translations
"\<P>(x in M. P)" => "CONST measure M {x \<in> CONST space M. P}"
@@ -324,10 +322,8 @@
syntax
"_conditional_prob" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic" (\<open>('\<P>'(_ in _. _ \<bar>/ _'))\<close>)
-
syntax_consts
"_conditional_prob" == cond_prob
-
translations
"\<P>(x in M. P \<bar> Q)" => "CONST cond_prob M (\<lambda>x. P) (\<lambda>x. Q)"