tidied
authorpaulson
Wed Jun 07 17:14:04 2000 +0200 (2000-06-07)
changeset 905380fca868ec4c
parent 9052 7db48fe85b05
child 9054 0e48e7d4d4f9
tidied
src/HOL/Real/RealOrd.ML
     1.1 --- a/src/HOL/Real/RealOrd.ML	Wed Jun 07 14:20:16 2000 +0200
     1.2 +++ b/src/HOL/Real/RealOrd.ML	Wed Jun 07 17:14:04 2000 +0200
     1.3 @@ -407,7 +407,7 @@
     1.4  by (EVERY1[dtac real_le_imp_less_or_eq, Step_tac]); 
     1.5  by (dtac real_mult_less_zero1 1 THEN assume_tac 1);
     1.6  by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym],
     1.7 -	      simpset() addsimps [real_minus_mult_eq1 RS sym]));
     1.8 +	      simpset()));
     1.9  qed "real_rinv_gt_zero";
    1.10  
    1.11  Goal "x < 0 ==> rinv x < 0";
    1.12 @@ -459,7 +459,7 @@
    1.13  by (rtac real_sum_gt_zero_less 1);
    1.14  by (dtac real_mult_order 1 THEN assume_tac 1);
    1.15  by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
    1.16 -    real_minus_mult_eq2 RS sym, real_mult_commute ]) 1);
    1.17 +					   real_mult_commute ]) 1);
    1.18  qed "real_mult_less_mono1";
    1.19  
    1.20  Goal "[| (0::real) < z; x < y |] ==> z*x < z*y";       
    1.21 @@ -738,7 +738,6 @@
    1.22  by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1);
    1.23  by (auto_tac (claset() addIs [real_mult_order],
    1.24  	      simpset() addsimps [real_add_assoc RS sym,
    1.25 -				  real_minus_mult_eq2 RS sym,
    1.26  				  real_minus_zero_less_iff2]));
    1.27  qed "real_mult_less_self";
    1.28  
    1.29 @@ -806,10 +805,7 @@
    1.30      [real_minus_zero_less_iff2,real_le_less]));
    1.31  qed "real_minus_zero_le_iff2";
    1.32  
    1.33 -Goal "-(x*x) <= (0::real)";
    1.34 -by (simp_tac (simpset() addsimps [real_minus_zero_le_iff2]) 1);
    1.35 -qed "real_minus_squre_le_zero";
    1.36 -Addsimps [real_minus_squre_le_zero];
    1.37 +Addsimps [real_minus_zero_le_iff, real_minus_zero_le_iff2];
    1.38  
    1.39  Goal "x * x + y * y = 0 ==> x = (0::real)";
    1.40  by (dtac real_add_minus_eq_minus 1);