equal
deleted
inserted
replaced
161 | ord => ord)) |
161 | ord => ord)) |
162 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) |
162 and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) |
163 end; |
163 end; |
164 |
164 |
165 val num_ss = |
165 val num_ss = |
166 simpset_of (put_simpset HOL_basic_ss @{context} |
166 simpset_of (put_simpset HOL_basic_ss @{context} |> Simplifier.set_term_ord numterm_ord); |
167 |> Simplifier.set_termless (is_less o numterm_ord)); |
|
168 |
167 |
169 (*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*) |
168 (*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*) |
170 val numeral_syms = [@{thm numeral_One} RS sym]; |
169 val numeral_syms = [@{thm numeral_One} RS sym]; |
171 |
170 |
172 (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) |
171 (*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) |