src/HOL/Bali/Evaln.thy

                  G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
 monos
   if_bool_eq_conj
 
 
-declare split_if     [split del] split_if_asm     [split del]
+declare if_split     [split del] if_split_asm     [split del]
         option.split [split del] option.split_asm [split del]
         not_None_eq [simp del] 
         split_paired_All [simp del] split_paired_Ex [simp del]
 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
 

         "G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
         "G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
         "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
 
-declare split_if     [split] split_if_asm     [split] 
+declare if_split     [split] if_split_asm     [split] 
         option.split [split] option.split_asm [split]
         not_None_eq [simp] 
         split_paired_All [simp] split_paired_Ex [simp]
 declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
 

 apply (tactic \<open>ALLGOALS (EVERY' [strip_tac @{context},
   TRY o eresolve_tac @{context} @{thms Suc_le_D_lemma},
   REPEAT o smp_tac @{context} 1, 
   resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW TRY o assume_tac @{context}])\<close>)
 (* 3 subgoals *)
-apply (auto split del: split_if)
+apply (auto split del: if_split)
 done
 
 lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
 
 lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow>