src/HOL/Mirabelle/Mirabelle.thy
author wenzelm
Mon, 24 Sep 2012 16:13:56 +0200
changeset 49550 0a82e98fd4a3
parent 48891 c0eafbd55de3
child 59574 de392405a851
permissions -rw-r--r--
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);
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
32381
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     7
begin
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     8
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47790
diff changeset
     9
ML_file "Tools/mirabelle.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47790
diff changeset
    10
ML_file "../TPTP/sledgehammer_tactics.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47790
diff changeset
    11
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    12
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
    13
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    14
ML {*
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    15
signature MIRABELLE_ACTION =
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    16
sig
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    17
  val invoke : (string * string) list -> theory -> theory
32381
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
    18
end
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    19
*}
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    20
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    21
end