src/HOL/Tools/Mirabelle/Mirabelle.thy
author boehmes
Fri, 21 Aug 2009 13:21:19 +0200
changeset 32385 594890623c46
parent 32383 521065a499c6
permissions -rw-r--r--
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32381
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     1
(* Title: Mirabelle.thy
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     2
   Author: Jasmin Blanchette and Sascha Boehme
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
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
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     8
begin
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     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
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    16
setup Mirabelle.setup
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    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
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    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