src/HOL/Real/RealBin.ML
changeset 9108 9fff97d29837
parent 9080 67ca888af420
child 9433 ac20534ce4d1
     1.1 --- a/src/HOL/Real/RealBin.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Real/RealBin.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -349,7 +349,7 @@
     1.4  		   real_mult_minus_1, real_mult_minus_1_right];
     1.5  
     1.6  (*To perform binary arithmetic*)
     1.7 -val bin_simps = 
     1.8 +val bin_simps =
     1.9      [add_real_number_of, real_add_number_of_left, minus_real_number_of, 
    1.10       diff_real_number_of] @ 
    1.11      bin_arith_simps @ bin_rel_simps;