# 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 ******)