src/HOL/Bali/WellForm.thy
changeset 51703 f2e92fc0c8aa
parent 47176 568fdc70e565
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Bali/WellForm.thy	Fri Apr 12 17:02:55 2013 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Fri Apr 12 17:21:51 2013 +0200
     1.3 @@ -2128,7 +2128,7 @@
     1.4  
     1.5  declare split_paired_All [simp del] split_paired_Ex [simp del]
     1.6  declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
     1.7 -declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
     1.8 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
     1.9  
    1.10  lemma dynamic_mheadsD:   
    1.11  "\<lbrakk>emh \<in> mheads G S statT sig;    
    1.12 @@ -2257,7 +2257,7 @@
    1.13    qed
    1.14  qed
    1.15  declare split_paired_All [simp] split_paired_Ex [simp]
    1.16 -declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
    1.17 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    1.18  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.19  
    1.20  (* Tactical version *)
    1.21 @@ -2402,7 +2402,7 @@
    1.22  
    1.23  declare split_paired_All [simp del] split_paired_Ex [simp del]
    1.24  declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
    1.25 -declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
    1.26 +setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
    1.27  
    1.28  lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow>  wf_prog (prg E) \<longrightarrow> 
    1.29    dt=empty_dt \<longrightarrow> (case T of 
    1.30 @@ -2426,7 +2426,7 @@
    1.31      )
    1.32  done
    1.33  declare split_paired_All [simp] split_paired_Ex [simp]
    1.34 -declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
    1.35 +setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    1.36  declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
    1.37  
    1.38  lemma ty_expr_is_type: