src/HOLCF/Ssum.thy
changeset 29063 7619f0561cd7
parent 27310 d0229bc6c461
child 29138 661a8db7e647
--- a/src/HOLCF/Ssum.thy	Thu Dec 11 16:30:35 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Thu Dec 11 16:50:18 2008 +0100
@@ -19,7 +19,7 @@
   "{p :: tr \<times> ('a \<times> 'b).
     (cfst\<cdot>p \<sqsubseteq> TT \<longleftrightarrow> csnd\<cdot>(csnd\<cdot>p) = \<bottom>) \<and>
     (cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
-by simp
+by simp_all
 
 instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
 by (rule typedef_finite_po [OF type_definition_Ssum])