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

more uniform syntax for named instantiations;

merged

added locale for semirings

exposed approximation in ML

clarified NEWS (cf. 97872c658a44);

clarified equality of formal entities;

merged

tuned signature;