src/HOL/MicroJava/J/TypeRel.thy
changeset 62390 842917225d56
parent 62145 5b946c81dfbf
child 67443 3abf6a722518
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Feb 23 15:37:18 2016 +0100
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Feb 23 16:25:08 2016 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4    method (G,C) = (if C = Object then empty else method (G,D)) ++  
     1.5    map_of (map (\<lambda>(s,m). (s,(C,m))) ms)"
     1.6  apply (unfold method_def)
     1.7 -apply (simp split del: split_if)
     1.8 +apply (simp split del: if_split)
     1.9  apply (erule (1) class_rec_lemma [THEN trans])
    1.10  apply auto
    1.11  done
    1.12 @@ -202,7 +202,7 @@
    1.13   fields (G,C) = 
    1.14    map (\<lambda>(fn,ft). ((fn,C),ft)) fs @ (if C = Object then [] else fields (G,D))"
    1.15  apply (unfold fields_def)
    1.16 -apply (simp split del: split_if)
    1.17 +apply (simp split del: if_split)
    1.18  apply (erule (1) class_rec_lemma [THEN trans])
    1.19  apply auto
    1.20  done