diff options
Diffstat (limited to 'lib/isabelle/Prompt_monad_lemmas.thy')
| -rw-r--r-- | lib/isabelle/Prompt_monad_lemmas.thy | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/isabelle/Prompt_monad_lemmas.thy b/lib/isabelle/Prompt_monad_lemmas.thy index 56aa6e87..84f3333e 100644 --- a/lib/isabelle/Prompt_monad_lemmas.thy +++ b/lib/isabelle/Prompt_monad_lemmas.thy @@ -4,6 +4,11 @@ theory Prompt_monad_lemmas Sail_values_lemmas begin +notation bind (infixr "\<bind>" 54) + +abbreviation seq :: "('rv,unit,'e)monad \<Rightarrow> ('rv,'b,'e)monad \<Rightarrow>('rv,'b,'e)monad" (infixr "\<then>" 54) where + "m \<then> n \<equiv> m \<bind> (\<lambda>_. n)" + lemma All_bind_dom: "bind_dom (m, f)" by (induction m) (auto intro: bind.domintros) |