tuned signature;

misc tuning for release;

merged

eliminated suspicious Unicode character;

eliminated hard tabs;

more standard access to goal state;

more standard Isabelle/ML tool setup; proper file headers; tuned whitespace;

added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);

proper test for session HOL-Library;

tuned;

tuned signature;

proper context for Object_Logic operations;

explicitly checked alpha conversion -- actual renaming happens outside kernel;

more standard access to specific subgoal;

tuned wording

updated 'old_smt' to loss of 'z3_non_commercial' option

Z3 news

updated certificates to latest Z3 (and took out one problem that no longer works)

updated docs to reflect actually run ATPs

reorder provers to reflect current eval results

updated docs to Z3 open source

updated SMT module and Sledgehammer to fully open source Z3

updated to new Z3

renamed multiset ordering to free up nice <# etc. symbols for the standard subset

removed TODO

consistent naming

merged

more lemmas and operations on cset (adapted from FSet)

tuned signature;

tuned;

misc tuning for release;

merged

Removed mcard because it is equal to size

generalized slightly

generalized code

generalized code

export ML function

recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;

more qualified names -- eliminated hide_const (open);

tuned;

merged

local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;

support for 'restricted' modifier: only qualified accesses outside the local scope;

tuned;

clarified rail syntax;

@{command_spec} is superseded by @{command_keyword};

clarified command keyword markup;

more position information and PIDE markup for command keywords;

allow prefix before keyword, notably 'private';

support local command setup;

proper header; misc tuning;

tuned signature;

tuned;

new theory Library/Tree_Multiset.thy

more standard local_theory command setup;

some explanation of 'private';

tuned message;

more general notion of command span: command keyword not necessarily at start; support for special 'private' prefix for local_theory commands; clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;

support private scope for individual local theory commands; tuned signature;

rearranged sessions to save approx. 1min elapsed time, 5min CPU time;

obsolete (see 8b7caf447357);

check wrt. proper context, e.g. relevant for 'experiment' target;

clarified name space policy: show less stuff in usual print functions;

unused;

more uniform "verbose" option to print name space;

tuned;

merged

proper treatment of internal method name as already checked Token.src;

tuned signature;

export for informative purposes;

sort constraints are inherent part of class abbreviations (in contrast to class constants)

semidom contains distributive minus, by convention

clarified method_closure; added option for Eisbach, which makes its own closure;

operation on embedded sources for Eisbach;

tuned signature;

tuned -- emphasize semantics of already checked src;

misc tuning -- keep name space more clean;

tuned;

merged

misc tuning -- keep name space more clean;

added command 'experiment';

imitate old "intern" semantics for the sake of outdated/unmaintained code, notably relevant for Simpl;

NEWS;

clarified "main" group, e.g. relevant for Isabelle/jEdit menu;

evade popular keyword;

tuned signature;

clarified module; more parallel processing;

ISABELLE_JAVA_SYSTEM_OPTIONS for scala REPL;

more reactive interrupts;

added isabelle build option -x, to exclude sessions;

added isabelle build option -k, for fast off-line checking of theory sources;

tuned signature;

tuned message;

tuned signature;

more visibility flags on background naming;

support for explicit scope of private entries;

subtle change of long-standing name space policy: unknown entries are treated as hidden, consequently "private" is understood in the strict sense;

tuned signature;

tuned signature;

tuned -- avoid exotic Name_Space.defined_entry;

tuned;

clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;

tuned;

tuned message;

more standard Long_Name operations;

tuned;

tuned;

tuned signature;

simplified code

Theorem "arctan" is no longer a default simprule

John Harrison's example: a 32-bit approximation to pi. SLOW

HOL Light Libraries for complex Arctan, Arcsin, Arccos

arcsin and arccos lemmas

NEWS

given up separate type classes demanding `inverse 0 = 0`

Merge

rationalised and generalised some theorems concerning abs and x^2.

added lemmas

Merge

New material and binomial fix

tuned doc

merged

tuned signature;

support for strictly private name space entries; tuned signature;

tuned signature;

export more low-level theorems in data structure (partly for 'corec')

tuned;

merged