equal
deleted
inserted
replaced
19 by (Asm_simp_tac 1); |
19 by (Asm_simp_tac 1); |
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); |
25 by (fast_tac HOL_cs 1); |
26 qed "bind_eq_Fail"; |
26 qed "bind_eq_Fail"; |
27 |
27 |
28 Addsimps [bind_eq_Fail]; |
28 Addsimps [bind_eq_Fail]; |