equal
deleted
inserted
replaced
20 qed "expand_bind"; |
20 qed "expand_bind"; |
21 |
21 |
22 goal Maybe.thy |
22 goal Maybe.thy |
23 "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; |
23 "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; |
24 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
24 by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
25 by (fast_tac HOL_cs 1); |
|
26 qed "bind_eq_Fail"; |
25 qed "bind_eq_Fail"; |
27 |
26 |
28 Addsimps [bind_eq_Fail]; |
27 Addsimps [bind_eq_Fail]; |