# HG changeset patch
# User wenzelm
# Date 1004445806 -3600
# Node ID 65e2822d83ddf0cd97404126b617c28c1f6f1132
# Parent  ad67e8d2c75f620b9803e0368bcb459d53e23228
lemma Least_mono moved from Typedef.thy to Set.thy;

diff -r ad67e8d2c75f -r 65e2822d83dd src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Oct 29 17:22:18 2001 +0100
+++ b/src/HOL/Set.thy	Tue Oct 30 13:43:26 2001 +0100
@@ -893,4 +893,15 @@
 use "equalities.ML"
 use "mono.ML"
 
+lemma Least_mono:
+  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
+    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
+    -- {* Courtesy of Stephan Merz *}
+  apply clarify
+  apply (erule_tac P = "%x. x : S" in LeastI2)
+   apply fast
+  apply (rule LeastI2)
+  apply (auto elim: monoD intro!: order_antisym)
+  done
+
 end
diff -r ad67e8d2c75f -r 65e2822d83dd src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Mon Oct 29 17:22:18 2001 +0100
+++ b/src/HOL/Typedef.thy	Tue Oct 30 13:43:26 2001 +0100
@@ -8,18 +8,6 @@
 theory Typedef = Set
 files ("Tools/typedef_package.ML"):
 
-lemma Least_mono: 
-  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
-    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
-    -- {* Courtesy of Stephan Merz *}
-  apply clarify
-  apply (erule_tac P = "%x. x : S" in LeastI2)
-   apply fast
-  apply (rule LeastI2)
-  apply (auto elim: monoD intro!: order_antisym)
-  done
-
-
 subsection {* HOL type definitions *}
 
 constdefs