# HG changeset patch
# User paulson
# Date 962182227 -7200
# Node ID 5b6b65c90eeb04636bb4435b7d6ccd5dddef0b20
# Parent  74d403974c8da59a163c8091e3198edcfce64341
got rid of weak elim rule

diff -r 74d403974c8d -r 5b6b65c90eeb src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Wed Jun 28 10:49:10 2000 +0200
+++ b/src/HOL/Integ/Equiv.ML	Wed Jun 28 10:50:27 2000 +0200
@@ -260,8 +260,8 @@
 by (rtac (Union_quotient RS subst) 1);
 by (assume_tac 1);
 by (rtac dvd_partition 1);
-by (blast_tac (claset() addEs [quotient_disj RS disjE]) 4);
+by (blast_tac (claset() addDs [quotient_disj]) 4);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [Union_quotient, equiv_type, 
-				      finite_quotient])));
+				       finite_quotient])));
 qed "equiv_imp_dvd_card";
diff -r 74d403974c8d -r 5b6b65c90eeb src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Wed Jun 28 10:49:10 2000 +0200
+++ b/src/HOL/Real/RealDef.ML	Wed Jun 28 10:50:27 2000 +0200
@@ -649,10 +649,14 @@
     addIs [preal_lemma_trans]) 1);
 qed "real_less_trans";
 
-Goal "!! (R1::real). [| R1 < R2; R2 < R1 |] ==> P";
+Goal "!! (R1::real). R1 < R2 ==> ~ (R2 < R1)";
+by (rtac notI 1);
 by (dtac real_less_trans 1 THEN assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [real_less_not_refl]) 1);
-qed "real_less_asym";
+qed "real_less_not_sym";
+
+(* [| x < y;  ~P ==> y < x |] ==> P *)
+bind_thm ("real_less_asym", real_less_not_sym RS swap);
 
 (****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
     (****** Map and more real_less ******)