src/HOL/HOLCF/Fixrec.thy
changeset 40834 a1249aeff5b6
parent 40795 c52cd8bc426d
child 41029 f7d8cfa6e7fc
     1.1 --- a/src/HOL/HOLCF/Fixrec.thy	Tue Nov 30 15:34:51 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Tue Nov 30 15:56:19 2010 -0800
     1.3 @@ -80,19 +80,17 @@
     1.4  
     1.5  text {* rewrite rules for mplus *}
     1.6  
     1.7 -lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose]
     1.8 -
     1.9  lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>"
    1.10  unfolding mplus_def
    1.11 -by (simp add: cont2cont_Rep_match Rep_match_strict)
    1.12 +by (simp add: cont_Rep_match Rep_match_strict)
    1.13  
    1.14  lemma mplus_fail [simp]: "fail +++ m = m"
    1.15  unfolding mplus_def fail_def
    1.16 -by (simp add: cont2cont_Rep_match Abs_match_inverse)
    1.17 +by (simp add: cont_Rep_match Abs_match_inverse)
    1.18  
    1.19  lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x"
    1.20  unfolding mplus_def succeed_def
    1.21 -by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse)
    1.22 +by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse)
    1.23  
    1.24  lemma mplus_fail2 [simp]: "m +++ fail = m"
    1.25  by (cases m, simp_all)