lib: fix unused/historical StateMonad theory
This commit is contained in:
parent
382b07dc20
commit
6aa78c310a
|
@ -149,7 +149,7 @@ declare
|
||||||
|
|
||||||
lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x"
|
lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x"
|
||||||
unfolding bindE_def return_def returnOk_def
|
unfolding bindE_def return_def returnOk_def
|
||||||
by (clarsimp simp: lift_def)
|
by (clarsimp simp: lift_def bind_def)
|
||||||
|
|
||||||
lemma lift_return [simp]:
|
lemma lift_return [simp]:
|
||||||
"lift (return \<circ> Inr) = return"
|
"lift (return \<circ> Inr) = return"
|
||||||
|
|
Loading…
Reference in New Issue