src/HOLCF/IOA/ABP/Correctness.thy
changeset 20918 b9068bd7255c
parent 19738 1ac610922636
child 25131 2c8caac48ade
equal deleted inserted replaced
20917:803c94363ccc 20918:b9068bd7255c
    59 
    59 
    60 declare let_weak_cong [cong]
    60 declare let_weak_cong [cong]
    61 declare Let_def [simp] ioa_triple_proj [simp] starts_of_par [simp]
    61 declare Let_def [simp] ioa_triple_proj [simp] starts_of_par [simp]
    62 
    62 
    63 lemmas env_ioas = env_ioa_def env_asig_def env_trans_def
    63 lemmas env_ioas = env_ioa_def env_asig_def env_trans_def
    64   and hom_ioas [simp] = env_ioas impl_ioas impl_trans impl_asigs asig_projections set_lemmas
    64 lemmas hom_ioas [simp] = env_ioas impl_ioas impl_trans impl_asigs asig_projections set_lemmas
    65 
    65 
    66 
    66 
    67 subsection {* lemmas about reduce *}
    67 subsection {* lemmas about reduce *}
    68 
    68 
    69 lemma l_iff_red_nil: "(reduce l = []) = (l = [])"
    69 lemma l_iff_red_nil: "(reduce l = []) = (l = [])"