--- a/src/HOL/Probability/Characteristic_Functions.thy	Tue Feb 13 17:18:57 2024 +0000
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Wed Feb 14 15:33:45 2024 +0000
@@ -56,8 +56,7 @@
 
 definition
   char :: "real measure \<Rightarrow> real \<Rightarrow> complex"
-where
-  "char M t = CLINT x|M. iexp (t * x)"
+  where "char M t \<equiv> CLINT x|M. iexp (t * x)"
 
 lemma (in real_distribution) char_zero: "char M 0 = 1"
   unfolding char_def by (simp del: space_eq_univ add: prob_space)