--- a/NEWS Thu Feb 17 19:00:14 2022 +0100
+++ b/NEWS Thu Feb 17 19:40:30 2022 +0100
@@ -57,10 +57,11 @@
- Replaced sledgehammer option "keep" by
"keep_probs", for problems files, and
"keep_proofs" for proof files. Minor INCOMPATIBILITY.
- - Added option "-r INT" to randomize the goals with a given seed before
+ - Added option "-r INT" to randomize the goals with a given 64-bit seed before
selection.
- Added option "-y" for a dry run.
- Renamed run_action to run in Mirabelle.action record. Minor INCOMPATIBILITY.
+ - Run the actions on goals before commands "unfolding" and "using".
* Meson
- Added support for polymorphic "using" facts. Minor INCOMPATIBILITY.
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Feb 17 19:00:14 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Feb 17 19:40:30 2022 +0100
@@ -187,7 +187,7 @@
(* presentation hook *)
-val whitelist = ["apply", "by", "proof"];
+val whitelist = ["apply", "by", "proof", "unfolding", "using"];
val _ =
Build.add_hook (fn qualifier => fn loaded_theories =>
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Feb 17 19:00:14 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Feb 17 19:40:30 2022 +0100
@@ -88,7 +88,7 @@
case List("mirabelle", action, "initialize") => action + " initialize "
case List("mirabelle", action, "finalize") => action + " finalize "
case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) =>
- action + " goal." + String.format("%-5s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " +
+ action + " goal." + String.format("%-9s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " +
args.theory_name + " " + line + ":" + offset + " "
case _ => ""
}