src/HOL/Datatype.thy
changeset 17876 b9c92f384109
parent 17458 e42bfad176eb
child 18230 4dc1f30af6a1
equal deleted inserted replaced
17875:d81094515061 17876:b9c92f384109
   167   "o2s (Some x) = {x}"
   167   "o2s (Some x) = {x}"
   168 
   168 
   169 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   169 lemma ospec [dest]: "(ALL x:o2s A. P x) ==> A = Some x ==> P x"
   170   by simp
   170   by simp
   171 
   171 
   172 ML_setup {* claset_ref() := claset() addSD2 ("ospec", thm "ospec") *}
   172 ML_setup {* change_claset (fn cs => cs addSD2 ("ospec", thm "ospec")) *}
   173 
   173 
   174 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   174 lemma elem_o2s [iff]: "(x : o2s xo) = (xo = Some x)"
   175   by (cases xo) auto
   175   by (cases xo) auto
   176 
   176 
   177 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"
   177 lemma o2s_empty_eq [simp]: "(o2s xo = {}) = (xo = None)"