changeset 2031 | 03a843f0f447 |
parent 1757 | f7a573c46611 |
child 2058 | ff04984186e9 |
--- a/src/HOL/MiniML/Maybe.ML Thu Sep 26 11:11:22 1996 +0200 +++ b/src/HOL/MiniML/Maybe.ML Thu Sep 26 12:47:47 1996 +0200 @@ -21,8 +21,8 @@ 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); +by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); +by (fast_tac HOL_cs 1); qed "bind_eq_Fail"; Addsimps [bind_eq_Fail];