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;

proper install_fonts;

proper jvmpath for Windows;

basic integration of graphview into document model; added Graph_Dockable; updated Isabelle/jEdit authors and dependencies etc.;

ML support for generic graph display, with browser and graphview backends (via print modes); reverse graph layout (again), according to the graph orientation provided by ML; simplified scala types -- eliminated unused type parameters; more explicit Model.Info, Model.Graph; renamed isabelle.graphview.Graphview_Frame to isabelle.graphview.Frame in accordance to file name; removed obsolete Graph_XML and Tooltips; tuned graphview command line; more generous JVM resources via GRAPHVIEW_JAVA_OPTIONS;

tuned;

more complete build; added option -c to imitate old browser;

proper error message;

separate module Graph_Display; tuned signature;

added graph encode/decode operations; tuned signature;

tuned;

minimal component and build setup for graphview;

added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;

made smlnj even happier

tuned proofs;

more explicit keyword1/keyword2 markup -- avoid potential conflict with input token markup produced by Token_Marker;

updated checksum, which appears to have changed accidentally;

updated to exec_process-1.0.2;

search bash via PATH as usual (this is no longer restricted to Cygwin with its known file-system layout);

discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);

Mirabelle appears to work better in single-threaded mode;

generalized types

tuned termination proof

adapted examples to new names

renamed coinduction principles to have "dtor" in the name

renamed "set_incl" etc. to have "ctor" or "dtor" in the name

renamed low-level "map_unique" to have "ctor" or "dtor" in the name

renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name