--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 29 20:08:08 2020 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 08 11:32:57 2020 +0200
@@ -11,6 +11,7 @@
has this pattern (provided it appears in a single line):
val .*K = "PARAMETER" (*DESCRIPTION*)
*)
+(* NOTE: Do not forget to update the Sledgehammer documentation to reflect changes here. *)
val check_trivialK = "check_trivial" (*=BOOL: check if goals are "trivial"*)
val e_selection_heuristicK = "e_selection_heuristic" (*=STRING: E clause selection heuristic*)