src/HOL/MiniML/Maybe.ML
changeset 3919 c036caebfc75
parent 2625 69c1b8a493de
child 4072 d0d32dd77440
equal deleted inserted replaced
3918:94e0fdcb7b91 3919:c036caebfc75
    23 by (Asm_simp_tac 1);
    23 by (Asm_simp_tac 1);
    24 qed "expand_option_bind";
    24 qed "expand_option_bind";
    25 
    25 
    26 goal thy
    26 goal thy
    27   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    27   "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    28 by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
    28 by(simp_tac (!simpset addsplits [expand_option_bind]) 1);
    29 qed "option_bind_eq_None";
    29 qed "option_bind_eq_None";
    30 
    30 
    31 Addsimps [option_bind_eq_None];
    31 Addsimps [option_bind_eq_None];
    32 
    32 
    33 (* auxiliary lemma *)
    33 (* auxiliary lemma *)