--- 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*)