# HG changeset patch
# User huffman
# Date 1227652004 -3600
# Node ID 1a1447cb6b7134129458a8b843005590121d952c
# Parent  9d19554bc2a08e24391fb3bc2c2a0612e6d57b99
renamed lemma compact_minimal to compact_bot_minimal

diff -r 9d19554bc2a0 -r 1a1447cb6b71 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Tue Nov 25 18:07:33 2008 +0100
+++ b/src/HOLCF/Universal.thy	Tue Nov 25 23:26:44 2008 +0100
@@ -666,7 +666,7 @@
     assume x_neq [simp]: "x \<noteq> compact_bot"
     with less have y_neq [simp]: "y \<noteq> compact_bot"
       apply clarify
-      apply (drule antisym_less [OF compact_minimal])
+      apply (drule antisym_less [OF compact_bot_minimal])
       apply simp
       done
     show ?case