--- 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];