--- a/src/HOL/Library/Open_State_Syntax.thy Wed Nov 11 23:06:27 2020 +0100
+++ b/src/HOL/Library/Open_State_Syntax.thy Thu Nov 12 09:06:44 2020 +0100
@@ -8,6 +8,10 @@
imports Main
begin
+context
+ includes state_combinator_syntax
+begin
+
subsection \<open>Motivation\<close>
text \<open>
@@ -55,9 +59,6 @@
again. To achieve this, we use a set of monad combinators:
\<close>
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
-
text \<open>
Given two transformations \<^term>\<open>f\<close> and \<^term>\<open>g\<close>, they may be
directly composed using the \<^term>\<open>(\<circ>>)\<close> combinator, forming a
@@ -111,6 +112,8 @@
lemmas monad_collapse = monad_simp fcomp_apply scomp_apply split_beta
+end
+
subsection \<open>Do-syntax\<close>