author  sultana 
Tue, 24 Apr 2012 13:59:29 +0100  
changeset 47730  15f4309bb9eb 
parent 47477  3fabf352243e 
child 47790  2e1636e45770 
permissions  rwrr 
32564  1 
(* Title: HOL/Mirabelle/Mirabelle.thy 
2 
Author: Jasmin Blanchette and Sascha Boehme, TU Munich 

32381  3 
*) 
4 

5 
theory Mirabelle 

41358
d5e91925916e
renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
blanchet
parents:
39155
diff
changeset

6 
imports Sledgehammer 
47730  7 
uses "Tools/mirabelle.ML" 
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
41358
diff
changeset

8 
"../ex/sledgehammer_tactics.ML" 
32381  9 
begin 
10 

39155  11 
(* no multithreading, no parallel proofs *) (* FIXME *) 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

12 
ML {* Multithreading.max_threads := 1 *} 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

13 
ML {* Goal.parallel_proofs := 0 *} 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

14 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

15 
ML {* Toplevel.add_hook Mirabelle.step_hook *} 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

16 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

17 
ML {* 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

18 
signature MIRABELLE_ACTION = 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

19 
sig 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

20 
val invoke : (string * string) list > theory > theory 
32381  21 
end 
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

22 
*} 
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

23 

594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset

24 
end 