equal
deleted
inserted
replaced
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 = Logic.mk_equals (t, sum) |
66 val goal = Logic.mk_equals (t, sum) |
67 in |
67 in |
68 Goal.prove ctxt [] [] goal (K (arith_tac ctxt 1)) |
68 Goal.prove ctxt [] [] goal (K (Arith_Data.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 |