src/HOL/Mirabelle/Mirabelle.thy
author sultana
Tue, 24 Apr 2012 13:59:29 +0100
changeset 47730 15f4309bb9eb
parent 47477 3fabf352243e
child 47790 2e1636e45770
permissions -rw-r--r--
reversed Tools to Actions Mirabelle renaming;
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
47730
15f4309bb9eb reversed Tools to Actions Mirabelle renaming;
sultana
parents: 47477
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