merged

tuned

operations to turn markup into XML; tuned;

removed obsolete org.w3c.dom operations;

eliminated obsolete HTML/CSS functionality;

removed obsolete Output1 dockable;

physical File.eq in conformance to Isabelle/ML;

tuned proofs;

tuned;

updated to consolidated SortedMap in scala-2.9.x;

partly ported "TreeFI" example to new syntax

avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)

tuned

tuned

merge

modernized examples; removed now trivial "HFset"

some support for jEdit warmstart;

discontinued XML.cache experiment -- Poly/ML 5.5.0 RTS does online sharing better;

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;