Summary
- merged
- proper build of required session images vs. build with Mirabelle presentation;
- reactive "sledgehammer";
- reactive "sledgehammer_filter": statically correct, but untested (no proof_file);
- clarified command-line;
- clarified signature; supporess empty results;
- clarified signature;
- clarified log content;
- reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
- tuned;
- unused;
- unused (see 8ffc607c345d);
- clarified signature: provide access to previous state;
- clarified signature (see Scala version);
- tuned signature;
- avoid duplicate loading of ML file;
The file was modified | src/HOL/Tools/Mirabelle/mirabelle.scala (diff) |
The file was modified | src/HOL/Mirabelle.thy (diff) |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle.ML (diff) |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML (diff) |
The file was modified | src/HOL/Mirabelle.thy (diff) |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML (diff) |
The file was modified | src/Pure/Concurrent/unsynchronized.ML (diff) |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle.scala (diff) |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle.ML (diff) |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle.scala (diff) |
The file was modified | src/Pure/Thy/export.scala (diff) |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle.scala (diff) |
The file was added | src/HOL/Mirabelle.thy |
The file was added | src/HOL/Tools/Mirabelle/mirabelle.ML |
The file was added | src/HOL/Tools/Mirabelle/mirabelle.scala |
The file was added | src/HOL/Tools/Mirabelle/mirabelle_arith.ML |
The file was added | src/HOL/Tools/Mirabelle/mirabelle_metis.ML |
The file was added | src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML |
The file was added | src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML |
The file was added | src/HOL/Tools/Mirabelle/mirabelle_sledgehammer_filter.ML |
The file was added | src/HOL/Tools/Mirabelle/mirabelle_try0.ML |
The file was modified | etc/components (diff) |
The file was modified | etc/options (diff) |
The file was modified | src/HOL/Main.thy (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff) |
The file was modified | src/HOL/Tools/etc/options (diff) |
The file was modified | src/Pure/General/path.scala (diff) |
The file was modified | src/Pure/Isar/token.ML (diff) |
The file was modified | src/Pure/Isar/toplevel.ML (diff) |
The file was modified | src/Pure/System/isabelle_tool.scala (diff) |
The file was modified | src/Pure/Thy/thy_info.ML (diff) |
The file was modified | src/Pure/build-jars (diff) |
The file was removed | src/HOL/Mirabelle/Mirabelle.thy |
The file was removed | src/HOL/Mirabelle/Mirabelle_Test.thy |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle.ML |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle_arith.ML |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle_metis.ML |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle_try0.ML |
The file was removed | src/HOL/Mirabelle/etc/settings |
The file was removed | src/HOL/Mirabelle/ex/Ex.thy |
The file was removed | src/HOL/Mirabelle/lib/Tools/mirabelle |
The file was removed | src/HOL/Mirabelle/lib/scripts/mirabelle.pl |
The file was modified | src/Pure/Isar/proof_context.ML (diff) |
The file was modified | src/Pure/Isar/parse.ML (diff) |
The file was modified | src/HOL/Mirabelle/Mirabelle_Test.thy (diff) |
The file was removed | src/HOL/Mirabelle/Tools/mirabelle_refute.ML |
The file was modified | src/Pure/Isar/toplevel.ML (diff) |
The file was modified | src/Pure/PIDE/document.ML (diff) |
The file was modified | src/Pure/Thy/thy_info.ML (diff) |
The file was modified | src/Pure/Thy/thy_output.ML (diff) |
The file was modified | src/Pure/Concurrent/par_list.ML (diff) |
The file was modified | src/Pure/Syntax/syntax_phases.ML (diff) |
The file was modified | src/HOL/Mirabelle/Tools/mirabelle.ML (diff) |
The file was added | src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML |
The file was modified | src/HOL/Mirabelle/Mirabelle.thy (diff) |
The file was modified | src/HOL/Sledgehammer.thy (diff) |
The file was modified | src/HOL/TPTP/ATP_Problem_Import.thy (diff) |
The file was modified | src/HOL/TPTP/TPTP_Parser_Example.thy (diff) |
The file was removed | src/HOL/TPTP/sledgehammer_tactics.ML |