src/HOL/MiniML/Maybe.ML
changeset 1751 946efd210837
parent 1300 c7a8f374339b
child 1757 f7a573c46611
equal deleted inserted replaced
1750:817a34a54fb0 1751:946efd210837
    16   "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
    16   "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
    17 by (maybe.induct_tac "res" 1);
    17 by (maybe.induct_tac "res" 1);
    18 by (fast_tac (HOL_cs addss !simpset) 1);
    18 by (fast_tac (HOL_cs addss !simpset) 1);
    19 by (Asm_simp_tac 1);
    19 by (Asm_simp_tac 1);
    20 qed "expand_bind";
    20 qed "expand_bind";
       
    21 
       
    22 goal Maybe.thy "!!x. x = Ok y ==> x ~= Fail";
       
    23 by(Asm_simp_tac 1);
       
    24 qed "eq_OkD";