src/HOL/Mirabelle/Mirabelle.thy
author nipkow
Wed, 20 Jan 2021 09:46:01 +0100
changeset 73139 be9b73dfd3e0
parent 69605 a96320074298
permissions -rw-r--r--
added lemmas
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
59574
de392405a851 import 'Main' to be on the safe side
blanchet
parents: 49550
diff changeset
     6
imports Main
32381
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     7
begin
11542bebe4d4 made Mirabelle a component
boehmes
parents:
diff changeset
     8
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 63167
diff changeset
     9
ML_file \<open>Tools/mirabelle.ML\<close>
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 63167
diff changeset
    10
ML_file \<open>../TPTP/sledgehammer_tactics.ML\<close>
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47790
diff changeset
    11
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 59574
diff changeset
    12
ML \<open>Toplevel.add_hook Mirabelle.step_hook\<close>
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    13
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 59574
diff changeset
    14
ML \<open>
32385
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
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 59574
diff changeset
    19
\<close>
32385
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