src/HOL/Datatype.thy
changeset 26339 7825c83c9eff
parent 26146 61cb176d0385
child 26356 2312df2efa12
equal deleted inserted replaced
26338:f8ed02f22433 26339:7825c83c9eff
   633   "o2s (Some x) = {x}"
   633   "o2s (Some x) = {x}"
   634 
   634 
   635 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   635 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   636   by simp
   636   by simp
   637 
   637 
   638 ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
   638 declaration {* fn _ =>
       
   639   Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
       
   640 *}
   639 
   641 
   640 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   642 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   641   by (cases xo) auto
   643   by (cases xo) auto
   642 
   644 
   643 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   645 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"