Theory HOL.Mirabelle

(*  Title:      HOL/Mirabelle.thy
    Author:     Jasmin Blanchette, TU Munich
    Author:     Sascha Boehme, TU Munich
    Author:     Makarius
    Author:     Martin Desharnais, UniBw Munich, MPI-INF Saarbrücken
*)

theory Mirabelle
  imports Sledgehammer Predicate_Compile Presburger
begin

ML_file ‹Tools/Mirabelle/mirabelle_util.ML›
ML_file ‹Tools/Mirabelle/mirabelle.ML›

ML ‹
signature MIRABELLE_ACTION = sig
  val make_action : Mirabelle.action_context -> string * Mirabelle.action
end
›

ML_file ‹Tools/Mirabelle/mirabelle_arith.ML›
ML_file ‹Tools/Mirabelle/mirabelle_order.ML›
ML_file ‹Tools/Mirabelle/mirabelle_metis.ML›
ML_file ‹Tools/Mirabelle/mirabelle_presburger.ML›
ML_file ‹Tools/Mirabelle/mirabelle_quickcheck.ML›
ML_file ‹Tools/Mirabelle/mirabelle_sledgehammer_filter.ML›
ML_file ‹Tools/Mirabelle/mirabelle_sledgehammer.ML›
ML_file ‹Tools/Mirabelle/mirabelle_try0.ML›

end