merged

make measure_of total

encode goal digest in spying log (to detect duplicates)

made SML/NJ happy

tuned proofs

use forthcoming "primcorec" command

set code and nitpick_simp attributes on primcorec theorems

tuning

tuned docs

register codatatypes with Nitpick

register codatatypes with Nitpick

don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)

added [code] to selectors

tuned spying

document "spy"

added "spy" option to Nitpick

document "spy" option

added "spy" option to Sledgehammer

proper text for document preparation;

set [code] on case equations

note coinduct theorems in "primcorec"

tuning

generate "simps" from "primcorec"

undid copy-paste

avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)

don't generate empty theorem collections

tuned code

provide a way to override MaSh's port from configuration file

new version of MaSh program, with proper shutdown

tuned proofs;