equal
deleted
inserted
replaced
61 | _ => raise TERM ("dest_sum", [term]) |
61 | _ => raise TERM ("dest_sum", [term]) |
62 |
62 |
63 fun get_sum_thm ctxt t (n1, n2) = |
63 fun get_sum_thm ctxt t (n1, n2) = |
64 let |
64 let |
65 val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2) |
65 val sum = HOLogic.mk_number @{typ "nat"} (n1 + n2) |
66 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, sum)) |
66 val goal = Logic.mk_equals (t, sum) |
67 in |
67 in |
68 mk_meta_eq (Goal.prove ctxt [] [] goal (K (simp_tac @{simpset} 1))) |
68 Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1)) |
69 end |
69 end |
70 |
70 |
71 fun add_sp_aux ss t = |
71 fun add_sp_aux ss t = |
72 let |
72 let |
73 val ctxt = Simplifier.the_context ss |
73 val ctxt = Simplifier.the_context ss |