11 local |
11 local |
12 |
12 |
13 val simprocs = field_cancel_numeral_factors |
13 val simprocs = field_cancel_numeral_factors |
14 |
14 |
15 val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, |
15 val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, |
16 inst "a" "(number_of ?v)" @{thm right_distrib}, |
16 OldGoals.inst "a" "(number_of ?v)" @{thm right_distrib}, |
17 @{thm divide_1}, @{thm divide_zero_left}, |
17 @{thm divide_1}, @{thm divide_zero_left}, |
18 @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
18 @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
19 @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, |
19 @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, |
20 @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, |
20 @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, |
21 @{thm of_int_minus}, @{thm of_int_diff}, |
21 @{thm of_int_minus}, @{thm of_int_diff}, |