| changeset 3919 | c036caebfc75 |
| parent 2625 | 69c1b8a493de |
| child 4072 | d0d32dd77440 |
--- a/src/HOL/MiniML/Maybe.ML Fri Oct 17 15:23:14 1997 +0200 +++ b/src/HOL/MiniML/Maybe.ML Fri Oct 17 15:25:12 1997 +0200 @@ -25,7 +25,7 @@ goal thy "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"; -by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); +by(simp_tac (!simpset addsplits [expand_option_bind]) 1); qed "option_bind_eq_None"; Addsimps [option_bind_eq_None];