src/HOL/Option.thy
changeset 39159 0dec18004e75
parent 39150 c4ff5fd8db99
child 39272 0b61951d2682
equal deleted inserted replaced
39158:e6b96b4cde7e 39159:0dec18004e75
    45 
    45 
    46 lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
    46 lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
    47   by simp
    47   by simp
    48 
    48 
    49 declaration {* fn _ =>
    49 declaration {* fn _ =>
    50   Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
    50   Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
    51 *}
    51 *}
    52 
    52 
    53 lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
    53 lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
    54   by (cases xo) auto
    54   by (cases xo) auto
    55 
    55