src/HOL/Mirabelle/Mirabelle.thy
author blanchet
Fri Apr 27 15:24:37 2012 +0200 (2012-04-27)
changeset 47790 2e1636e45770
parent 47730 15f4309bb9eb
child 48891 c0eafbd55de3
permissions -rw-r--r--
move file to where it belongs
     1 (*  Title:      HOL/Mirabelle/Mirabelle.thy
     2     Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     3 *)
     4 
     5 theory Mirabelle
     6 imports Sledgehammer
     7 uses "Tools/mirabelle.ML"
     8      "../TPTP/sledgehammer_tactics.ML"
     9 begin
    10 
    11 (* no multithreading, no parallel proofs *)  (* FIXME *)
    12 ML {* Multithreading.max_threads := 1 *}
    13 ML {* Goal.parallel_proofs := 0 *}
    14 
    15 ML {* Toplevel.add_hook Mirabelle.step_hook *}
    16 
    17 ML {*
    18 signature MIRABELLE_ACTION =
    19 sig
    20   val invoke : (string * string) list -> theory -> theory
    21 end
    22 *}
    23 
    24 end