src/HOL/Mirabelle/Mirabelle.thy
author wenzelm
Sat, 12 Sep 2009 16:30:48 +0200
changeset 32564 378528d2f7eb
parent 32496 4ab00a2642c3
child 39155 3e94ebe282f1
permissions -rw-r--r--
standard headers and text sections;
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
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