document antiquotations for ML infix operators;

tuned;

updated repetition tacticals; discontinued odd trace_REPEAT (assumes sequential TTY loop);

updated THEN, ORELSE, APPEND, and derivatives; discontinued obscure INTLEAVE;

removed obscure/outdated material;

updated RSN, RL, RLN, MRS; discontinued obscure MRL;

removed obscure/outdated material;

tuned;

more on Logic.all/mk_implies etc.;

reduce AFP test by many hours;

added termination of narrowing

really need 64bit here; prefer explicit version information for contrib;

Added termination proof for widening

switch afp test to Darwin on macbroy2

merged

introduced commands over a set of vars

basic support for PIDE Scala programming, independently of the main Isabelle repository;

fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick

updated message

improve installation instructions

allow use of proxy for remote SMT solver invocations, just like in the "remote_atp" script

factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero

refreshing NEWS

renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)

renamed theory AList to DAList

position constraints for numerals enable PIDE markup;

more careful cumulation of tooltips -- ensure uniform range;

tuned;

tuned

missing dependency

tuned example;

merged

back to more basic caret_range (reverting 0ad063afa3d6) -- BreakIterator crashes due to non-zero text.offset when deleting the first character of the buffer;

recovered outdated_color (cf. 4beb2f41ed93);

more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;

tuned proofs;

tuned

tuned signature;

comments;

tuned proofs;

eliminated dead code, together with spurious warning about congruence rule for "Fun.comp";

more explicit/robust treatment of common snapshot;

discontinued old-style Term.list_abs in favour of plain Term.abs;

renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;

renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;

tuned;

discontinued old-style Term.list_all_free in favour of plain Logic.all;

tuned;

discontinued default rendering for Oheimb's double-space;

tuned white space;

tuned comment;

paranoia null check -- prevent spurious crash of jedit token markup;

tuned comments;

tuned signature;

clarified partial restrict operation;

tuned proofs;

ignore empty gfx_range; tuned;

tuned signature;

tuned

handle specific exception, not arbitrary ones (including Interrupt);

eliminated dead code;

more modest settings for lxbroy10 -- might actually perform better;

tuned;

improved select_markup: include filtering of defined results;

tuned text_color: cumulate with explicit default color;

added cat_lines convenience;

tuned;

clarified mkString: no extra line-breaks for XML.Body;

adding exhaustive instances for type constructor set

Updated generated file

Added inf_Int_eq to pred_set_conv database as well

more conventional eval_tac vs. method_setup "eval"; clarified method "normalization": THEN_ALL_NEW avoids bumping into other subgoals;

updated generated file -- change of printed case syntax probably due to f805747f8571;

actually try to preserve names given by user (cf. 463b594e186a);

updated example -- List.foldl is no longer defined via primrec;

more qualified names; more antiquotations;

refer to imp_cong from HOL, not Drule (!) -- cf. 4ed94d92ae19;

more robust ISABELLE_HOME_USER for repository versions -- some versions of Emacs interpret foo//bar as /bar even on the command-line (unlike regular POSIX semantics);

merged

Removed strange hack introduced in b27e93132603, since equivariance is working again

Replaced perm_set_eq by perm_set_def

Corrected pt_set_inst, added missing cp_set_inst, deleted obsolete pt_insert_eqvt, pt_set_eqvt, and perm_set_eq

Reverted several lemmas involving sets to the state before the removal of the set type.

clarified Isabelle_Rendering vs. physical painting; discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;

pred_subset_eq and SUP_UN_eq2 are now standard pred_set_conv rules

pred_subset/equals_eq are now standard pred_set_conv rules

Declared pred_equals/subset_eq, sup_Un_eq and SUP_UN_eq(2) as pred_set_conv rules

merged

add simp rules for set_bit and msb applied to 0 and 1

add simp rule test_bit_1

proper hiding of facts and constants in AList_Impl and AList theory

NEWS

adding quickcheck examples with multisets

improving code generation for multisets; adding exhaustive quickcheck generators for multisets

adding theory association lists with invariant

command status color via regular markup;