tuned message;

merged

disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)

got rid of other instance of shaky "Thm.generalize"

tweaked theorem names (in particular, dropped s's)

get rid of shaky "Thm.generalize"

fixed "rels" + split them into injectivity and distinctness

generate high-level "coinduct" and "strong_coinduct" properties

added coinduction tactic

generalized tactic a bit

export "dtor_map_coinduct" theorems, since they're used in one example

name tuning

parameterized "subst_tac"

generate high-level "maps", "sets", and "rels" properties

use singular since there is always only one theorem

nicer type var names

renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"

renamed "dtor_coinduct" etc. to "dtor_map_coinduct"

leave out some internal theorems unless "bnf_note_all" is set

tuned

added counterexamples

tuned

tuned

more uniform graphview terminology;

proper Symbol.decode -- especially relevant for Proof General;

suppress empty tooltips;

obsolete;

updated keywords;

more uniform graphview terminology;

tuned pretty_locale/print_locale, with more basic pretty_locale_deps based on that; added command 'locale_deps'; graphview prints plain text only -- removed dependency on old Cobra HTML_Panel;