src/HOL/Mirabelle/Mirabelle.thy
author wenzelm
Mon Sep 24 16:13:56 2012 +0200 (2012-09-24)
changeset 49550 0a82e98fd4a3
parent 48891 c0eafbd55de3
child 59574 de392405a851
permissions -rw-r--r--
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);
     1 (*  Title:      HOL/Mirabelle/Mirabelle.thy
     2     Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     3 *)
     4 
     5 theory Mirabelle
     6 imports Sledgehammer
     7 begin
     8 
     9 ML_file "Tools/mirabelle.ML"
    10 ML_file "../TPTP/sledgehammer_tactics.ML"
    11 
    12 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    13 
    14 ML {*
    15 signature MIRABELLE_ACTION =
    16 sig
    17   val invoke : (string * string) list -> theory -> theory
    18 end
    19 *}
    20 
    21 end