src/HOL/Option.ML
changeset 4032 4b1c69d8b767
parent 3344 b3e39a2987c1
child 4071 4747aefbbc52
equal deleted inserted replaced
4031:42cbf6256d60 4032:4b1c69d8b767
     4     Copyright   1996  TU Muenchen
     4     Copyright   1996  TU Muenchen
     5 
     5 
     6 Derived rules
     6 Derived rules
     7 *)
     7 *)
     8 
     8 
     9 open Option;
     9 val expand_option_case = split_option_case;
    10 
       
    11 goal Option.thy "P(case opt of None => a | Some(x) => b x) = \
       
    12 \                ((opt = None --> P a) & (!x. opt = Some x --> P(b x)))";
       
    13 by (option.induct_tac "opt" 1);
       
    14 by (Simp_tac 1);
       
    15 by (Asm_full_simp_tac 1);
       
    16 qed "expand_option_case";