| changeset 39979 | b13515940b53 |
| parent 39978 | 11bfb7e7cc86 |
| child 40157 | a2f01956220e |
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Oct 11 18:02:14 2010 +0700 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Oct 11 18:03:18 2010 +0700 @@ -9,6 +9,7 @@ signature METIS_TACTICS = sig + val trace : bool Config.T val type_lits : bool Config.T val new_skolemizer : bool Config.T val metis_tac : Proof.context -> thm list -> int -> tactic