| changeset 3919 | c036caebfc75 |
| parent 2520 | aecaa76e7eff |
| child 4089 | 96fba19bcbe2 |
--- a/src/HOL/W0/Maybe.ML Fri Oct 17 15:23:14 1997 +0200 +++ b/src/HOL/W0/Maybe.ML Fri Oct 17 15:25:12 1997 +0200 @@ -26,7 +26,7 @@ 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 (simp_tac (!simpset addsplits [expand_bind]) 1); qed "bind_eq_Fail"; Addsimps [bind_eq_Fail];