1.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy	Thu Feb 18 12:36:09 2010 -0800
     1.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Thu Feb 18 13:29:59 2010 -0800
     1.3 @@ -57,10 +57,12 @@
     1.4    and impl_asigs = sender_asig_def receiver_asig_def
     1.5  
     1.6  declare let_weak_cong [cong]
     1.7 -declare Let_def [simp] ioa_triple_proj [simp] starts_of_par [simp]
     1.8 +declare ioa_triple_proj [simp] starts_of_par [simp]
     1.9  
    1.10  lemmas env_ioas = env_ioa_def env_asig_def env_trans_def
    1.11 -lemmas hom_ioas [simp] = env_ioas impl_ioas impl_trans impl_asigs asig_projections set_lemmas
    1.12 +lemmas hom_ioas =
    1.13 +  env_ioas [simp] impl_ioas [simp] impl_trans [simp] impl_asigs [simp]
    1.14 +  asig_projections set_lemmas
    1.15  
    1.16  
    1.17  subsection {* lemmas about reduce *}
    1.18 @@ -96,7 +98,7 @@
    1.19  apply (induct_tac "l")
    1.20  apply (simp (no_asm))
    1.21  apply (case_tac "list=[]")
    1.22 - apply (simp add: reverse.simps)
    1.23 + apply simp
    1.24   apply (rule impI)
    1.25  apply (simp (no_asm))
    1.26  apply (cut_tac l = "list" in cons_not_nil)