# HG changeset patch
# User oheimb
# Date 982249244 -3600
# Node ID bdfb9ec76a0ad248cfe0b201b1e64e734bdb98c0
# Parent  9265b6415d76ffc9f9d5173b88004bf4f16193e5
simplified proof of Least_mono

diff -r 9265b6415d76 -r bdfb9ec76a0a src/HOL/mono.ML
--- a/src/HOL/mono.ML	Thu Feb 15 16:00:42 2001 +0100
+++ b/src/HOL/mono.ML	Thu Feb 15 16:00:44 2001 +0100
@@ -105,15 +105,14 @@
                    ex_mono, Collect_mono, in_mono];
 
 (* Courtesy of Stephan Merz *)
-Goalw [Least_def,mono_def]
-  "[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
+Goalw [Least_def] 
+"[| mono (f::'a::order => 'b::order); ? x:S. ! y:S. x <= y |] \
 \  ==> (LEAST y. y : f`S) = f(LEAST x. x : S)";
-by (etac bexE 1);
-by (rtac someI2 1);
-by (Force_tac 1);
-by (rtac some_equality 1);
-by (Force_tac 1);
-by (force_tac (claset() addSIs [order_antisym], simpset()) 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("P","%x. x : S")] LeastMI2 1);
+by  (Fast_tac 1);
+by (rtac LeastMI2 1);
+by (auto_tac (claset() addEs [monoD] addSIs [thm "order_antisym"], simpset()));
 qed "Least_mono";
 
 Goal "[| a = b; c = d; b --> d |] ==> a --> c";