src/HOLCF/One.thy

--- a/src/HOLCF/One.thy	Wed Oct 12 01:43:37 2005 +0200
+++ b/src/HOLCF/One.thy	Wed Oct 12 03:01:09 2005 +0200
@@ -45,4 +45,7 @@
 apply simp_all
 done
 
+lemma compact_ONE [simp]: "compact ONE"
+by (rule compact_chfin)
+
 end