--- 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";
--- 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 ******)