--- a/src/HOL/Tools/nat_numeral_simprocs.ML Fri Oct 28 16:49:15 2011 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML Sat Oct 29 10:00:35 2011 +0200
@@ -365,7 +365,6 @@
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
- val prove_conv = Arith_Data.prove_conv
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
end;
--- a/src/HOL/Tools/numeral_simprocs.ML Fri Oct 28 16:49:15 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Oct 29 10:00:35 2011 +0200
@@ -470,7 +470,6 @@
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
val simplify_meta_eq = cancel_simplify_meta_eq
- val prove_conv = Arith_Data.prove_conv
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
end;
--- a/src/Provers/Arith/extract_common_term.ML Fri Oct 28 16:49:15 2011 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Sat Oct 29 10:00:35 2011 +0200
@@ -23,7 +23,6 @@
val find_first: term -> term list -> term list
(*proof tools*)
val mk_eq: term * term -> term
- val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
val norm_tac: simpset -> tactic (*proves the result*)
val simplify_meta_eq: simpset -> thm -> thm -> thm (*simplifies the result*)
val simp_conv: simpset -> term -> thm option (*proves simp thm*)