src/HOL/Mirabelle/Mirabelle.thy
author wenzelm
Wed Aug 22 22:55:41 2012 +0200 (2012-08-22)
changeset 48891 c0eafbd55de3
parent 47790 2e1636e45770
child 49550 0a82e98fd4a3
permissions -rw-r--r--
prefer ML_file over old uses;
     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 (* no multithreading, no parallel proofs *)  (* FIXME *)
    13 ML {* Multithreading.max_threads := 1 *}
    14 ML {* Goal.parallel_proofs := 0 *}
    15 
    16 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    17 
    18 ML {*
    19 signature MIRABELLE_ACTION =
    20 sig
    21   val invoke : (string * string) list -> theory -> theory
    22 end
    23 *}
    24 
    25 end