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 =