src/HOL/MicroJava/BV/Listn.thy
changeset 10918 9679326489cd
parent 10496 f2d304bdf3cc
child 11225 01181fdbc9f0
     1.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 00:38:59 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Tue Jan 16 00:40:57 2001 +0100
     1.3 @@ -340,7 +340,7 @@
     1.4    "!!L. semilat L ==> semilat (Listn.sl n L)"
     1.5  apply (unfold Listn.sl_def)
     1.6  apply (simp (no_asm_simp) only: split_tupled_all)
     1.7 -apply (simp (no_asm) only: semilat_Def Product_Type.split)
     1.8 +apply (simp (no_asm) only: semilat_Def split_conv)
     1.9  apply (rule conjI)
    1.10   apply simp
    1.11  apply (rule conjI)
    1.12 @@ -471,7 +471,7 @@
    1.13    "err_semilat (A,r,f) ==> 
    1.14    err_semilat (list n A, Listn.le r, sup f)"
    1.15  apply (unfold Err.sl_def)
    1.16 -apply (simp only: Product_Type.split)
    1.17 +apply (simp only: split_conv)
    1.18  apply (simp (no_asm) only: semilat_Def plussub_def)
    1.19  apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
    1.20  apply (rule conjI)