src/HOL/Real/Hyperreal/HyperDef.ML
changeset 9043 ca761fe227d8
parent 9013 9dd0274f76af
child 9055 f020e00c6304
     1.1 --- a/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 07 12:07:07 2000 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Wed Jun 07 12:14:18 2000 +0200
     1.3 @@ -587,29 +587,29 @@
     1.4  Goal "-(x * y) = -x * (y::hypreal)";
     1.5  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
     1.6  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
     1.7 -by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
     1.8 -    hypreal_mult,real_minus_mult_eq1] 
     1.9 -      @ real_mult_ac @ real_add_ac));
    1.10 +by (auto_tac (claset(),
    1.11 +	      simpset() addsimps [hypreal_minus, hypreal_mult] 
    1.12 +                                 @ real_mult_ac @ real_add_ac));
    1.13  qed "hypreal_minus_mult_eq1";
    1.14  
    1.15  Goal "-(x * y) = (x::hypreal) * -y";
    1.16  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    1.17  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
    1.18  by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
    1.19 -   hypreal_mult,real_minus_mult_eq2] 
    1.20 -    @ real_mult_ac @ real_add_ac));
    1.21 +					   hypreal_mult] 
    1.22 +                                           @ real_mult_ac @ real_add_ac));
    1.23  qed "hypreal_minus_mult_eq2";
    1.24  
    1.25  Goal "-x*-y = x*(y::hypreal)";
    1.26  by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
    1.27 -    hypreal_minus_mult_eq1 RS sym]) 1);
    1.28 +				       hypreal_minus_mult_eq1 RS sym]) 1);
    1.29  qed "hypreal_minus_mult_cancel";
    1.30  
    1.31  Addsimps [hypreal_minus_mult_cancel];
    1.32  
    1.33  Goal "-x*y = (x::hypreal)*-y";
    1.34  by (full_simp_tac (simpset() addsimps [hypreal_minus_mult_eq2 RS sym,
    1.35 -    hypreal_minus_mult_eq1 RS sym]) 1);
    1.36 +				       hypreal_minus_mult_eq1 RS sym]) 1);
    1.37  qed "hypreal_minus_mult_commute";
    1.38  
    1.39