author  boehmes 
Fri, 21 Aug 2009 13:21:19 +0200  
changeset 32385  594890623c46 
parent 32383  521065a499c6 
permissions  rwrr 
32381  1 
(* Title: Mirabelle.thy 
2 
Author: Jasmin Blanchette and Sascha Boehme 

3 
*) 

4 

5 
theory Mirabelle 

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

6 
imports Pure 
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
32381
diff
changeset

7 
uses "Tools/mirabelle.ML" 
32381  8 
begin 
9 

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

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

11 
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

12 
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

13 

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

14 
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

15 

32381  16 
setup Mirabelle.setup 
17 

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

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

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

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

21 
val invoke : (string * string) list > theory > theory 
32381  22 
end 
32385
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 

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

25 
end 