equal
deleted
inserted
replaced
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); |
|
31 qed"expand_option_case"; |
30 qed"expand_option_case"; |