src/HOL/Bali/Evaln.thy
changeset 62390 842917225d56
parent 62042 6c6ccf573479
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Bali/Evaln.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4    if_bool_eq_conj
     1.5  
     1.6  
     1.7 -declare split_if     [split del] split_if_asm     [split del]
     1.8 +declare if_split     [split del] if_split_asm     [split del]
     1.9          option.split [split del] option.split_asm [split del]
    1.10          not_None_eq [simp del] 
    1.11          split_paired_All [simp del] split_paired_Ex [simp del]
    1.12 @@ -234,7 +234,7 @@
    1.13          "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
    1.14          "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
    1.15  
    1.16 -declare split_if     [split] split_if_asm     [split] 
    1.17 +declare if_split     [split] if_split_asm     [split] 
    1.18          option.split [split] option.split_asm [split]
    1.19          not_None_eq [simp] 
    1.20          split_paired_All [simp] split_paired_Ex [simp]
    1.21 @@ -453,7 +453,7 @@
    1.22    REPEAT o smp_tac @{context} 1, 
    1.23    resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW TRY o assume_tac @{context}])\<close>)
    1.24  (* 3 subgoals *)
    1.25 -apply (auto split del: split_if)
    1.26 +apply (auto split del: if_split)
    1.27  done
    1.28  
    1.29  lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]