generalize proof reconstruction code;

first step towards support for nonnumeric formula names, needed for E 1.2

first step towards support for nonnumeric formula names, needed for E 1.2

handle relevance filter corner cases more gracefully;

e.g. the minimizer selects 15 facts but "max_relevant = 14"

e.g. the minimizer selects 15 facts but "max_relevant = 14"

src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer.ML src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

Sledgehammer should be called in "prove" mode;

otherwise the proof text won't fit into the proof document

otherwise the proof text won't fit into the proof document

adapt examples to latest Nitpick changes + speed them up a little bit

src/HOL/Nitpick_Examples/Integer_Nits.thy src/HOL/Nitpick_Examples/Manual_Nits.thy src/HOL/Nitpick_Examples/Typedef_Nits.thy

eliminate more clutter related to "fast_descrs" optimization

src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_kodkod.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Nitpick/nitpick_mono.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML

remove "fast_descs" option from Nitpick;

the option has been unsound for over a year and is too imprecise to be of any use when made sound

the option has been unsound for over a year and is too imprecise to be of any use when made sound

doc-src/Nitpick/nitpick.tex src/HOL/Nitpick_Examples/Core_Nits.thy src/HOL/Nitpick_Examples/Mono_Nits.thy src/HOL/Tools/Nitpick/nitpick.ML src/HOL/Tools/Nitpick/nitpick_hol.ML src/HOL/Tools/Nitpick/nitpick_isar.ML src/HOL/Tools/Nitpick/nitpick_model.ML src/HOL/Tools/Nitpick/nitpick_mono.ML src/HOL/Tools/Nitpick/nitpick_nut.ML src/HOL/Tools/Nitpick/nitpick_preproc.ML