src/HOLCF/Ssum.thy
changeset 29530 9905b660612b
parent 29138 661a8db7e647
child 31076 99fe356cbbc2
--- a/src/HOLCF/Ssum.thy	Wed Jan 14 13:47:14 2009 -0800
+++ b/src/HOLCF/Ssum.thy	Wed Jan 14 17:11:29 2009 -0800
@@ -188,7 +188,7 @@
 
 lemma beta_sscase:
   "sscase\<cdot>f\<cdot>g\<cdot>s = (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s)"
-unfolding sscase_def by (simp add: cont_Rep_Ssum)
+unfolding sscase_def by (simp add: cont_Rep_Ssum cont2cont_LAM)
 
 lemma sscase1 [simp]: "sscase\<cdot>f\<cdot>g\<cdot>\<bottom> = \<bottom>"
 unfolding beta_sscase by (simp add: Rep_Ssum_strict)