src/HOL/Mirabelle/Mirabelle.thy
changeset 47477 3fabf352243e
parent 42616 92715b528e78
child 47730 15f4309bb9eb
equal deleted inserted replaced
47476:92d1c566ebbf 47477:3fabf352243e
     2     Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     2     Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
     3 *)
     3 *)
     4 
     4 
     5 theory Mirabelle
     5 theory Mirabelle
     6 imports Sledgehammer
     6 imports Sledgehammer
     7 uses "Tools/mirabelle.ML"
     7 uses "Actions/mirabelle.ML"
     8      "../ex/sledgehammer_tactics.ML"
     8      "../ex/sledgehammer_tactics.ML"
     9 begin
     9 begin
    10 
    10 
    11 (* no multithreading, no parallel proofs *)  (* FIXME *)
    11 (* no multithreading, no parallel proofs *)  (* FIXME *)
    12 ML {* Multithreading.max_threads := 1 *}
    12 ML {* Multithreading.max_threads := 1 *}