src/HOL/Mirabelle/Mirabelle.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42616 92715b528e78
child 47477 3fabf352243e
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32564
378528d2f7eb standard headers and text sections;
wenzelm
parents: 32496
diff changeset
     1
(*  Title:      HOL/Mirabelle/Mirabelle.thy
378528d2f7eb standard headers and text sections;
wenzelm
parents: 32496
diff changeset
     2
    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
32381
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     3
*)
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     4
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     5
theory Mirabelle
41358
d5e91925916e renamed "sledgehammer_tactic.ML" to "sledgehammer_tactics.ML" (cf. module name);
blanchet
parents: 39155
diff changeset
     6
imports Sledgehammer
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents: 32381
diff changeset
     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
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     9
begin
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    10
39155
3e94ebe282f1 some results of concurrency code inspection;
wenzelm
parents: 32564
diff changeset
    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
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    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