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;

ind_cases: clarified preparation of arguments;

support for minimal specifications, with usual treatment of fixes and dummies;

tuned;

tuned;

tuned signature;

proper local Proof_Context.arity_sorts;

more standard Sign.typ_match: sorts should be alright in result of Syntax.check_terms;

avoid low-level tsig operations;

tuned;

clarified context;

rule_insts_schematic is considered legacy and false by default;

tuned;

clarified no_zero_devisors: makes only sense in a semiring; actually turn linorder_semidom into a integral domain

dropped long-outdated comments

merged

clarified goal context;

clarified goal context;

prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;

proper Rule_Insts.read_term, e.g. to enable case_tac using "_";

tuned signature;

clarified goal context;

clarified doc

more graceful failure if some of the involved BNFs have no data

sort BNFs in output

preserve order of type arguments in pre-FP BNF typedef

register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')

store low-level (un)fold constants

export more functions

restored broken metis proof

distributivity of partial minus establishes desired properties of dvd in semirings

explicit commutative additive inverse operation; more explicit focal point for commutative monoids with an inverse operation

modernized

more multiset theorems

semantic completion for @{system_option};

clarified position;

HOL-SPARK .prv files are subject to system option spark_prv; tuned;

tuned signature;

NEWS;

prefer local fixes;

proper signature; tuned;

dummies may depend on goal params as well;

merged

proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;

clarified case_tac fixes and context;

clarified name;

option to control old-style schematic mode;

clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;

tuned;

tuned proof;

admit dummy patterns in instantiations; clarified context;

clarified input source;

tuning

reordered properties

NEWS;

tuned proof;

implicit goal parameters are improper;

merged

prefer local fixes;

local fixes may depend on goal params;

tuned;

clarified syntax category "fixes";

tuned signature;

tuned syntax diagrams -- no duplication of "target";

tuned;

tuned;

support 'for' fixes in rule_tac etc.;

fix parameter order of NO_MATCH

add measurable_submarkov

BT subsumed by Library/Tree

added funs and lemmas

tuned;

tuned;

tuned;

tuned;

read instantiations uniformly for rules and tactics; tuned;

removed presumably pointless detail;

tuned;

tuned;

make SML/NJ happy;

Merge

tweaked a few slow or very ugly proofs

merged

tuned signature;

tuned;

tuned signature;

tuned;

tuned -- prepare instantiation more uniformly;

Merge

fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!

merged

more position information;

misc tuning;

tuned;

Merge

New material for complex sin, cos, tan, Ln, also some reorganisation

updated to sumatra_pdf-3.0;

tuned comments;

slightly more formal historic examples;

bounded powerset

new HOL Light material about exp, sin, cos

new file for complex transcendental functions

Merge

Merge

Merge

Lots of new material on complex-valued functions. Modified simplification of (x/n)^k

merged

added proof method rewrite

merged

tuned;

tight span for theory header, which is relevant for error positions (including semantic completion);

misc tuning and simplification;

Inserted real_of_nat to fix factorial-related problem

more general type class for factorial. Now allows code generation (?)

Merge

Merge

The factorial function, "fact", now has type "nat => 'a"

merged

added lemmas

document property

BNF relators preserve reflexivity

export more ML functions

merged

suppress semantic completion in errors of batch build -- avoid junk in log files;

updated docs

clarified documentation

proper headers;

merged

tuned message -- include completion;

support for completion reports produced in Scala (inlined into messages);

more precises positions; more permissive imports;

avoid duplicate header errors, more precise positions; tuned signature;

tuned protocol -- resolve command positions in ML;

clarified modules;

add inequalities (move from AFP/Amortized_Complexity)

merge

inlining threshold

avoid controversial Pirate syntax

more markup, which helps to create missing imports;

tuned signature;

proper command id for inlined errors, which is important for Command.State.accumulate;

clarified span position;

tuned;

tuned;

hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;

more command categories, as in ML; tuned;

more command categories, as in ML;

tuned;

value-oriented user error, for well-defined Thy_Syntax.chop_common;

more explicit exception User_Error, with value-oriented equality;

tuned signature;