| changeset 1757 | f7a573c46611 |
| parent 1751 | 946efd210837 |
| child 2031 | 03a843f0f447 |
--- a/src/HOL/MiniML/Maybe.ML Wed May 22 16:54:16 1996 +0200 +++ b/src/HOL/MiniML/Maybe.ML Wed May 22 17:11:54 1996 +0200 @@ -19,6 +19,10 @@ by (Asm_simp_tac 1); qed "expand_bind"; -goal Maybe.thy "!!x. x = Ok y ==> x ~= Fail"; -by(Asm_simp_tac 1); -qed "eq_OkD"; +goal Maybe.thy + "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; +by(simp_tac (!simpset setloop (split_tac [expand_bind])) 1); +by(fast_tac HOL_cs 1); +qed "bind_eq_Fail"; + +Addsimps [bind_eq_Fail];