diff -r 4747aefbbc52 -r d0d32dd77440 src/HOL/MiniML/Maybe.ML --- a/src/HOL/MiniML/Maybe.ML Mon Nov 03 09:57:35 1997 +0100 +++ b/src/HOL/MiniML/Maybe.ML Mon Nov 03 09:58:06 1997 +0100 @@ -16,16 +16,14 @@ Addsimps [option_bind_Some,option_bind_None]; (* expansion of option_bind *) -goal thy - "P(option_bind res f) = ((res = None --> P None) & (!s. res = Some s --> P(f s)))"; -by (option.induct_tac "res" 1); -by (fast_tac (HOL_cs addss !simpset) 1); -by (Asm_simp_tac 1); -qed "expand_option_bind"; +goalw thy [option_bind_def] "P(option_bind res f) = \ +\ ((res = None --> P None) & (!s. res = Some s --> P(f s)))"; +br split_option_case 1; +qed "split_option_bind"; goal thy "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"; -by(simp_tac (!simpset addsplits [expand_option_bind]) 1); +by(simp_tac (!simpset addsplits [split_option_bind]) 1); qed "option_bind_eq_None"; Addsimps [option_bind_eq_None];