| changeset 2058 | ff04984186e9 |
| parent 2031 | 03a843f0f447 |
| child 2525 | 477c05586286 |
--- a/src/HOL/MiniML/Maybe.ML Mon Oct 07 10:31:50 1996 +0200 +++ b/src/HOL/MiniML/Maybe.ML Mon Oct 07 10:34:58 1996 +0200 @@ -22,7 +22,6 @@ 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];