src/HOL/Option.ML
changeset 8423 3c19160b6432
parent 7030 53934985426a
child 8442 96023903c2df
equal deleted inserted replaced
8422:6c6a5410a9bd 8423:3c19160b6432
    80 
    80 
    81 claset_ref() := claset() addSD2 ("ospec", ospec);
    81 claset_ref() := claset() addSD2 ("ospec", ospec);
    82 
    82 
    83 
    83 
    84 Goal "x : o2s xo = (xo = Some x)";
    84 Goal "x : o2s xo = (xo = Some x)";
    85 by (exhaust_tac "xo" 1);
    85 by (cases_tac "xo" 1);
    86 by Auto_tac;
    86 by Auto_tac;
    87 qed "elem_o2s";
    87 qed "elem_o2s";
    88 AddIffs [elem_o2s];
    88 AddIffs [elem_o2s];
    89 
    89 
    90 Goal "(o2s xo = {}) = (xo = None)";
    90 Goal "(o2s xo = {}) = (xo = None)";
    91 by (exhaust_tac "xo" 1);
    91 by (cases_tac "xo" 1);
    92 by Auto_tac;
    92 by Auto_tac;
    93 qed "o2s_empty_eq";
    93 qed "o2s_empty_eq";
    94 
    94 
    95 Addsimps [o2s_empty_eq];
    95 Addsimps [o2s_empty_eq];
    96 
    96