src/HOL/Tools/res_axioms.ML
changeset 17905 1574533861b1
parent 17829 35123f89801e
child 17959 8db36a108213
--- a/src/HOL/Tools/res_axioms.ML	Tue Oct 18 17:59:37 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Wed Oct 19 06:33:24 2005 +0200
@@ -23,6 +23,7 @@
   val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
   val clause_setup : (theory -> theory) list
   val meson_method_setup : (theory -> theory) list
+  val pairname : thm -> (string * thm)
   end;
 
 structure ResAxioms : RES_AXIOMS =