1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Wed Sep 02 16:23:53 2009 +0200
     1.3 @@ -0,0 +1,25 @@
     1.4 +(* Title:  mirabelle_metis.ML
     1.5 +   Author: Jasmin Blanchette and Sascha Boehme
     1.6 +*)
     1.7 +
     1.8 +structure Mirabelle_Metis : MIRABELLE_ACTION =
     1.9 +struct
    1.10 +
    1.11 +fun metis_action {pre, post, timeout, log} =
    1.12 +  let
    1.13 +    val thms = Mirabelle.theorems_of_sucessful_proof post
    1.14 +    val names = map Thm.get_name thms
    1.15 +    val add_info = if null names then I else suffix (":\n" ^ commas names)
    1.16 +
    1.17 +    val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
    1.18 +
    1.19 +    fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
    1.20 +  in
    1.21 +    (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
    1.22 +    |> add_info
    1.23 +    |> log
    1.24 +  end
    1.25 +
    1.26 +fun invoke _ = Mirabelle.register ("metis", metis_action)
    1.27 +
    1.28 +end