changeset 29713 | 55c30d1117ef |
parent 28287 | c86fa4e0aedb |
child 30304 | d8e4cd2ac2a1 |
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Mon Feb 02 15:12:18 2009 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Mon Feb 02 15:12:22 2009 +0100 @@ -8,8 +8,8 @@ signature LEXICOGRAPHIC_ORDER = sig val lexicographic_order : thm list -> Proof.context -> Method.method + val lexicographic_order_tac : Proof.context -> tactic -> tactic - (* exported for debugging *) val setup: theory -> theory end