src/HOL/HOLCF/Ssum.thy
changeset 40834 a1249aeff5b6
parent 40774 0437dbc127b3
child 42151 4da4fc77664b
     1.1 --- a/src/HOL/HOLCF/Ssum.thy	Tue Nov 30 15:34:51 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Ssum.thy	Tue Nov 30 15:56:19 2010 -0800
     1.3 @@ -172,7 +172,7 @@
     1.4  
     1.5  lemma beta_sscase:
     1.6    "sscase\<cdot>f\<cdot>g\<cdot>s = (\<lambda>(t, x, y). If t then f\<cdot>x else g\<cdot>y) (Rep_ssum s)"
     1.7 -unfolding sscase_def by (simp add: cont_Rep_ssum [THEN cont_compose])
     1.8 +unfolding sscase_def by (simp add: cont_Rep_ssum)
     1.9  
    1.10  lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
    1.11  unfolding beta_sscase by (simp add: Rep_ssum_strict)