equal
deleted
inserted
replaced
122 (case Rat.dest x of (i, 1) => i | _ => error "int_of_rat: bad int")), |
122 (case Rat.dest x of (i, 1) => i | _ => error "int_of_rat: bad int")), |
123 conv = (fn ctxt => |
123 conv = (fn ctxt => |
124 Simplifier.rewrite (put_simpset semiring_norm_ss ctxt) |
124 Simplifier.rewrite (put_simpset semiring_norm_ss ctxt) |
125 then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}))}; |
125 then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_One}))}; |
126 |
126 |
127 val divide_const = Thm.cterm_of @{context} (Logic.varify_global @{term "op /"}); |
127 val divide_const = Thm.cterm_of @{context} (Logic.varify_global @{term "(/)"}); |
128 val [divide_tvar] = Term.add_tvars (Thm.term_of divide_const) []; |
128 val [divide_tvar] = Term.add_tvars (Thm.term_of divide_const) []; |
129 |
129 |
130 val field_funs = |
130 val field_funs = |
131 let |
131 let |
132 fun numeral_is_const ct = |
132 fun numeral_is_const ct = |