Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed lemma compact_minimal to compact_bot_minimal
authorhuffman
Tue, 25 Nov 2008 23:26:44 +0100
changeset 28889 1a1447cb6b71
parent 28888 9d19554bc2a0
child 28890 1a36f0050734
renamed lemma compact_minimal to compact_bot_minimal
src/HOLCF/Universal.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle