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;

proper cumulation of bulk arguments;

tuned;

merge

revert unintended "sledgehammer" call

prefer antiquotations;

misc tuning and reformatting;

updated generated file;

Added termination to IMP Abs_Int

added lemmas

massaging of code setup for sets

dropped theory More_Set

use Inf/Sup_bool_def/apply as code equations

tuned

accumulate status as regular markup for command range; tuned signature;

corrected slip

tuned

restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)

moved lemmas about List.set and set operations to List theory

moved lemmas about List.set and set operations to List theory

incorporated various theorems from theory More_Set into corpus

consolidated various theorem names relating to Finite_Set.fold and List.fold combinators

merged

farewell to theory More_List

dropped unused nth_map

more explicit NEWS

refined case syntax again, improved treatment of constructors without arguments, e.g. "case a of (True, x) => x";

tuned;

improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;

tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);

recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);

more careful treatment of outermost constraints, e.g. constructors without arguments (despite loss of positions for catch-all variables);

proper refs;

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)

incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r); tuned quotes

prefer listsum over foldl plus 0

prefer concat over foldl append []

tuned proofs

interaction of set operations for execution and membership predicate

cleanup of code declarations

discontinued Syntax.positions -- atomic parse trees are always annotated;