src/HOL/Option.ML
changeset 2031 03a843f0f447
parent 2019 b45d9f2042e0
child 2056 93c093620c28
equal deleted inserted replaced
2030:474b3f208789 2031:03a843f0f447
    25 goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
    25 goal Option.thy "P(case opt of None => a | Some(x) => b(x)) = \
    26 \                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
    26 \                ((opt = None --> P a) & (!x. opt = Some x --> P(b(x))))";
    27 by (option.induct_tac "opt" 1);
    27 by (option.induct_tac "opt" 1);
    28 by (Simp_tac 1);
    28 by (Simp_tac 1);
    29 by (Asm_full_simp_tac 1);
    29 by (Asm_full_simp_tac 1);
    30 by(Fast_tac 1);
    30 by (Fast_tac 1);
    31 qed"expand_option_case";
    31 qed"expand_option_case";