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

renamed "map_simps" to "{c,d}tor_maps"

took out accidentally submitted "tracing" calls

fixed bug in "fold" tactic with nested products (beyond the sum of product corresponding to constructors)

simplified fact policies

generate "rel_as_srel" and "rel_flip" properties

started work on generation of "rel" theorems

make smlnj happy

more strict typscheme_equiv check: must fix variables of more specific type; dropped dead code; tuned order

cache should not contain material from descendant theory

some PIDE NEWS from this summer;

tuned whitespace;

tuned;

tuned proofs;

report proper binding positions only -- avoid swamping document model with unspecific information;

accumulate under exec_id as well;

more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);

misc tuning;

Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;

tuned signature;

tuned proofs;

misc tuning;

tighten margin for TextArea instead of Lobo;

misc tuning;

renamed LFP low-level rel property to have ctor not dtor in its name

changed base session for "HOL-BNF" for faster building in the typical case

renamed "rel_simp" to "dtor_rel" and similarly for "srel"

fixed a few names that escaped the renaming

tuned whitespace

merged

clean up lemmas used for composition

created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term

renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"

renamed top-level theory from "Codatatype" to "BNF"

adapted examples to renamings

renamed "pred" to "rel" (relator)

renamed "rel" to "srel"

fixed bug introduced by fold/unfold renaming

renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)

simplified code

tuned a few ML names

renamed "fld"/"unf" to "ctor"/"dtor"

tuning

renamed "upto" coinduction "strong"

tuned variable names

tuned names

more termination proofs

rel_Gr does not depend on map_wpull

renamed Output to Output1 and Output2 to Output, and thus make the new version the default;

more realistic sendback: pick exec_id from message position and text from buffer;

some support for hovering and sendback area;

merged

tuned antiquotations

merged

use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;

conected CS to big-step

generate "expand" property

merge

finished "disc_coiter_iff" etc. generation

the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)

generate coiter_iff and corec_iff theorems