author  wenzelm 
Mon, 24 Sep 2012 16:13:56 +0200  
changeset 49550  0a82e98fd4a3 
parent 48891  c0eafbd55de3 
child 59574  de392405a851 
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 
32381  7 
begin 
8 

48891  9 
ML_file "Tools/mirabelle.ML" 
10 
ML_file "../TPTP/sledgehammer_tactics.ML" 

11 

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

12 
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

13 

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

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

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

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

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

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

20 

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

21 
end 