src/HOL/Bali/AxSound.thy
changeset 62390 842917225d56
parent 62042 6c6ccf573479
child 67443 3abf6a722518
     1.1 --- a/src/HOL/Bali/AxSound.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/Bali/AxSound.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -1356,12 +1356,12 @@
     1.4            proof -
     1.5              from s2_no_return s3
     1.6              have "abrupt s3 \<noteq> Some (Jump Ret)"
     1.7 -              by (cases s2) (auto simp add: init_lvars_def2 split: split_if_asm)
     1.8 +              by (cases s2) (auto simp add: init_lvars_def2 split: if_split_asm)
     1.9              moreover
    1.10              obtain abr2 str2 where s2: "s2=(abr2,str2)"
    1.11                by (cases s2)
    1.12              from s3 s2 conf_s2 have "(abrupt s3,str2)\<Colon>\<preceq>(G, L)"
    1.13 -              by (auto simp add: init_lvars_def2 split: split_if_asm)
    1.14 +              by (auto simp add: init_lvars_def2 split: if_split_asm)
    1.15              ultimately show ?thesis
    1.16                using s3 s2 eq_s3'_s3
    1.17                apply (simp add: init_lvars_def2)
    1.18 @@ -1661,7 +1661,7 @@
    1.19            by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
    1.20          moreover note s3
    1.21          ultimately show ?thesis 
    1.22 -          by (force split: split_if)
    1.23 +          by (force split: if_split)
    1.24        qed
    1.25        with R v s4 
    1.26        have "R \<lfloor>v\<rfloor>\<^sub>e s4 Z"
    1.27 @@ -1923,7 +1923,7 @@
    1.28        from wt obtain  
    1.29          wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
    1.30          wt_then_else: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
    1.31 -        by cases (simp split: split_if)
    1.32 +        by cases (simp split: if_split)
    1.33        from da obtain E S where
    1.34          da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
    1.35          da_then_else: 
    1.36 @@ -2587,7 +2587,7 @@
    1.37          from this wt_super wf
    1.38          have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
    1.39            by - (rule eval_statement_no_jump 
    1.40 -                 [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"], auto split: split_if)
    1.41 +                 [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"], auto split: if_split)
    1.42          with conf_s1
    1.43          show ?thesis
    1.44            by (cases s1) (auto intro: conforms_set_locals)