--- a/src/HOL/Probability/PMF_Impl.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Probability/PMF_Impl.thy Thu Nov 12 09:06:44 2020 +0100
@@ -539,11 +539,11 @@
(Code_Evaluation.valtermify (+) {\<cdot>} A {\<cdot>}
(Code_Evaluation.valtermify single {\<cdot>} x))"
+instantiation pmf :: (random) random
+begin
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
-instantiation pmf :: (random) random
+context
+ includes state_combinator_syntax
begin
definition
@@ -555,8 +555,7 @@
end
-no_notation fcomp (infixl "\<circ>>" 60)
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+end
instantiation pmf :: (full_exhaustive) full_exhaustive
begin