--- 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