src/HOL/Option.thy
changeset 51703 f2e92fc0c8aa
parent 51096 60e4b75fefe1
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Option.thy	Fri Apr 12 17:02:55 2013 +0200
     1.2 +++ b/src/HOL/Option.thy	Fri Apr 12 17:21:51 2013 +0200
     1.3 @@ -46,9 +46,7 @@
     1.4  lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
     1.5    by simp
     1.6  
     1.7 -declaration {* fn _ =>
     1.8 -  Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
     1.9 -*}
    1.10 +setup {* map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec})) *}
    1.11  
    1.12  lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
    1.13    by (cases xo) auto