src/HOL/HOLCF/ex/Pattern_Match.thy
changeset 40834 a1249aeff5b6
parent 40774 0437dbc127b3
child 41229 d797baa3d57c
     1.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Nov 30 15:34:51 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Tue Nov 30 15:56:19 2010 -0800
     1.3 @@ -63,7 +63,7 @@
     1.4    "match_bind\<cdot>fail\<cdot>k = fail"
     1.5    "match_bind\<cdot>(succeed\<cdot>x)\<cdot>k = k\<cdot>x"
     1.6  unfolding match_bind_def fail_def succeed_def
     1.7 -by (simp_all add: cont2cont_Rep_match cont_Abs_match
     1.8 +by (simp_all add: cont_Rep_match cont_Abs_match
     1.9    Rep_match_strict Abs_match_inverse)
    1.10  
    1.11  subsection {* Case branch combinator *}