# HG changeset patch
# User blanchet
# Date 1443713728 -7200
# Node ID 9f9b088d882456f046d630d87944cd4968a406a9
# Parent  484f7878ede4498e552d3ae3a93e3dc620b0763b
export proof method in signature

diff -r 484f7878ede4 -r 9f9b088d8824 src/HOL/Tools/Metis/metis_tactic.ML
--- 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