diff -r 21238c9d363e -r a129b817b58a src/HOL/MiniML/Maybe.ML --- a/src/HOL/MiniML/Maybe.ML Tue Dec 16 15:17:26 1997 +0100 +++ b/src/HOL/MiniML/Maybe.ML Tue Dec 16 17:58:03 1997 +0100 @@ -18,17 +18,17 @@ (* expansion of 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; +by (rtac 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 [split_option_bind]) 1); +by (simp_tac (simpset() addsplits [split_option_bind]) 1); qed "option_bind_eq_None"; Addsimps [option_bind_eq_None]; (* auxiliary lemma *) goal Maybe.thy "(y = Some x) = (Some x = y)"; -by( simp_tac (simpset() addsimps [eq_sym_conv]) 1); +by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1); qed "rotate_Some";