--- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Oct 01 17:32:07 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Oct 01 17:35:28 2015 +0200
@@ -16,6 +16,8 @@
val metis_tac_unused : string list -> string -> Proof.context -> thm list -> int -> thm ->
thm list * thm Seq.seq
val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
+ val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list ->
+ thm -> thm Seq.seq
val metis_lam_transs : string list
val parse_metis_options : (string list option * string option) parser
end