src/HOL/Bali/Evaln.thy
changeset 51717 9e7d1c139569
parent 46714 a7ca72710dfe
child 52037 837211662fb8
     1.1 --- a/src/HOL/Bali/Evaln.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4          option.split [split del] option.split_asm [split del]
     1.5          not_None_eq [simp del] 
     1.6          split_paired_All [simp del] split_paired_Ex [simp del]
     1.7 -declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
     1.8 +setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
     1.9  
    1.10  inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
    1.11  
    1.12 @@ -238,7 +238,7 @@
    1.13          option.split [split] option.split_asm [split]
    1.14          not_None_eq [simp] 
    1.15          split_paired_All [simp] split_paired_Ex [simp]
    1.16 -declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.17 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *}
    1.18  
    1.19  lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
    1.20    (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)