equal
deleted
inserted
replaced
22 real_mult_0, real_mult_0_right, |
22 real_mult_0, real_mult_0_right, |
23 real_mult_1, real_mult_1_right, |
23 real_mult_1, real_mult_1_right, |
24 real_mult_minus_1, real_mult_minus_1_right]; |
24 real_mult_minus_1, real_mult_minus_1_right]; |
25 |
25 |
26 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ |
26 val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@ |
27 Real_Numeral_Simprocs.cancel_numerals(* @ real_cancel_numeral_factors*); |
27 Real_Numeral_Simprocs.cancel_numerals; |
28 |
28 |
29 val mono_ss = simpset() addsimps |
29 val mono_ss = simpset() addsimps |
30 [real_add_le_mono,real_add_less_mono, |
30 [real_add_le_mono,real_add_less_mono, |
31 real_add_less_le_mono,real_add_le_less_mono]; |
31 real_add_less_le_mono,real_add_le_less_mono]; |
32 |
32 |