eliminated spurious fact duplicates;

modernized dynamic "rules" -- avoid rebinding of static facts;

removed redundant lemma, cf. class zero_neq_one in HOL/Rings.thy;

clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;

tuned;

clarified Local_Defs.add_def(s): refrain from hard-wiring Thm.def_binding_optional; clarified Generic_Target.define: avoid duplicate def binding via Local_Defs.add_def;

more explicit flags for facts table;

minor tuning;

more conventional Double constants;

tuned source structure;

tuned;

tuned;

merged

added type annotations to generated Isar proofs -- code by Steffen Smolka

consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common

corrected NEWS

avoid somewhat heavy rebuilding of SortedMap via map where plain iteration is sufficient; more elementary level_list: avoid stack overflow; prefer elementary graph operations; tuned;

clarified long_names -- conform to usual Isabelle practice of not analysing internal names;

more precise repaint and revalidate -- the latter is important to keep in sync with content update;

tuned;

prefer synchronous Mutator_Event.Bus on Swing_Thread;

more direct tooltip content;

tuned;

use Pretty_Tooltip for Graphview_Panel; tuned signature;

more basic tooltips;

close tooltips more thoroughly;

make buttons closer to original mouse position;

detach tooltip as dockable window;

explicit close button;

congruence rule for Finite_Set.fold

alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^

eliminated obsolete tooltip delay -- bypassed by Pretty_Tooltip;

merged

newer versions of Z3 call it "Bool" not "bool"

simplified type of msetprod; n.b. image function need not be part of minimal definition of msetprod, since multisets may already contain repeated elements

tuned proof

default simp rule for image under identity

dropped duplicate facts; tuned syntax

more facts on setsum and setprod

made SML/NJ happier

do not expose details of internal data structures for composition of BNFs

further support for nested tooltips;

tuned proofs;

refer to parent frame -- relevant for floating dockables in particular;

tuned window position to fit on screen;

tuned window position;

determine window size from content;

tuned color and font size;

close tooltip window on escape; tuned;

proper message markup for output;

some re-ordering of initialization to ensure proper formatting;

separate module Pretty_Tooltip;

refined rich tooltip options; basic tooltips without markup;

Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin;

some documentation of show_markup;

tuned proofs;

option to bypass potentially slow text overview;

tuned signature;

clarified platform dependency;

updated crontab and afp-poly settings

thread the right local theory through + reenable parallel proofs for previously problematic theories

made code more conform to rest of BNF package

more error positions;

more explicit show_type_constraint, show_sort_constraint;

recovered print translation after 'a => bool to 'a set change;

tuned;

use explicit Type.strip_sorts_dummy to suppress sort constraints in output;

printed "_ofsort" is subject to show_markup as well;

allow position constraints to coexist with 0 or 1 sort constraints; more position information in sorting error; report sorting of all type variables;

made tactic more robust (less usage of stac)

continued changing type of corec type

removed dead params and dead code

changed type of corecursor for the nested recursion case

made (co)rec tactic more robust when the simplifier succeeds early

tuned;

removed unused module Blob;

more direct message header: eliminated historic encoding via single letter;

tuned whitespace;

tuned proofs;

report sort assignment of visible type variables;

more robust File.eq, and thus File.copy of "~~/lib/logo/isabelle.gif";

fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)

tweaked corecursor/coiterator tactic

changed the type of the recursor for nested recursion

fixed quick-and-dirty mode

tuning

use Thm.close_derivation in theorems proved using Skip_Proof.prove; tuned signature;

got rid of subst_tac alias

tuned tactic

tuned proofs;

tuned proofs;

proper handling of constraints stemming from idtyp_ast_tr';

enable show_markup by default (approx. double output size);

more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;

explicit show_types takes preferenced over show_markup;

ignore wrapped markup elements in Proof General;

turn constraints into Isabelle_Markup.typing, depending on show_markup options; proper recursion in standard_format;

treat wrapped markup elements as raw markup delimiters;

tuned signature;

tuned proofs;

tuned proofs;

tuned proofs;

tuned;

support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

merged

eliminated dead code;

smarter handling of tracing messages;

display number of tracing messages;

tuned signature;

tuned proofs;

simplified simpset

fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"

tuned tactic

updated keywords using proper "isabelle update_keywords";

tuned tactic

tuned tactic

merge

renamed ML file in preparation for next step

killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"

modernized example, exploiting "rep_compat" option

compatibility option to use "rep_datatype"

tuned message

modernized example

tuned tactics

second usage of const_typ

new antiquotation const_typ

tuned printing of _ in latex

mk_readable_rsp_thm_eq is more robust now

new get function for non-symmetric relator_eq & tuned

merged

tuned tactic; got rid of substs_tac alias

use a nicer scheme to indexify names

tuned tactic

type of the bound of a BNF depends at most on dead type variables

repaired signature

lower the defaults for the number of bits, based on an example by Lukas Bulwahn

modernized examples

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;

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