equal
deleted
inserted
replaced
162 ["t + u::'a::ring", |
162 ["t + u::'a::ring", |
163 "t - u::'a::ring", |
163 "t - u::'a::ring", |
164 "t * u::'a::ring", |
164 "t * u::'a::ring", |
165 "- t::'a::ring"]; |
165 "- t::'a::ring"]; |
166 fun proc sg ss t = |
166 fun proc sg ss t = |
167 let val rew = Tactic.prove sg [] [] |
167 let val rew = Goal.prove sg [] [] |
168 (HOLogic.mk_Trueprop |
168 (HOLogic.mk_Trueprop |
169 (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) |
169 (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t)))) |
170 (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) |
170 (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1) |
171 |> mk_meta_eq; |
171 |> mk_meta_eq; |
172 val (t', u) = Logic.dest_equals (Thm.prop_of rew); |
172 val (t', u) = Logic.dest_equals (Thm.prop_of rew); |