src/HOL/Bali/AxSem.thy
changeset 24019 67bde7cfcf10
parent 23894 1a4167d761ac
child 24038 18182c4aec9e
     1.1 --- a/src/HOL/Bali/AxSem.thy	Sat Jul 28 20:40:20 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Jul 28 20:40:22 2007 +0200
     1.3 @@ -471,10 +471,8 @@
     1.4  declare split_paired_All [simp del] split_paired_Ex [simp del] 
     1.5  declare split_if     [split del] split_if_asm     [split del] 
     1.6          option.split [split del] option.split_asm [split del]
     1.7 -ML_setup {*
     1.8 -change_simpset (fn ss => ss delloop "split_all_tac");
     1.9 -change_claset (fn cs => cs delSWrapper "split_all_tac");
    1.10 -*}
    1.11 +declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    1.12 +declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
    1.13  
    1.14  inductive
    1.15    ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
    1.16 @@ -1015,9 +1013,7 @@
    1.17  apply  (auto simp add: type_ok_def)
    1.18  done
    1.19  
    1.20 -ML {*
    1.21 -bind_thms ("ax_Abrupts", sum3_instantiate (thm "ax_derivs.Abrupt"))
    1.22 -*}
    1.23 +ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *}
    1.24  declare ax_Abrupts [intro!]
    1.25  
    1.26  lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]