default value for parametricity of dim

added lemma

clarified signature: more uniform theory_message (see also d7920eb7de54);

tuned -- use existing operation;

merged

isabelle emacs no longer exists;

utilize 'flip'

comments

merged

reorient -> split; documented split

merged

Added tag Isabelle2018-RC0 for changeset 194fa3d2d6a4

merged

resolution of name clashes in Algebra

merged

isabelle update_comments;

tuned header;

updated for release;

updated for release;

misc tuning and updates for release;

updated for release;

updated for release; tuned;

eliminated suspicious Unicode;

proper white space;

updated to sqlite-jdbc-3.23.1;

merged

Keep filter input syntax

more parallelism to cope with 8h30 CPU time;

full benchmarks, including all conditional theories;

tuned proofs;

more robust;

less wasteful consolidation, based on PIDE front-end state and recent changes;

tuned -- short-circuit result;

tuned;

updated URLs;

merged

more robust;

avoid hardwired cygwin mirror;

updated to current Cygwin, after 2.10.0-1 from 02-Feb-2018; record cygwin mirror explicitly;

NEWS: infinite products

merged

more tweaks of Cauchy

clarified signature; simplified options;

tuned proofs;

NEWS;

proper function invocation with all arguments;

fork parallel prints early in execution: avoid degradation of priority due to main eval task;

clarified signature: prefer Document.Snapshot;

list syntax details

merged

allow tuple patterns in list comprehensions

infinite product material

merged

tidied more Cauchy proofs

tuned proofs;

more symbols;

more formal comments;

more args;

record active execution task and depend on it -- avoid new executions bumping into old ones;

tuned -- more explicit types;

less frequent consolidation: it requires a full Document.update and Document.start_execution;

varify frees, notably dangling_params (see also e0cd57aeb60c);

tuned -- more explicit expression;

merged

documentation for "isabelle dump";

more dump aspects, with options; tuned signature;

tuned signature;

clarified default: all aspects;

clarified priority;

merged

added lemma

Fixed latex markup

merged

more tidying

merged

more symbols;

Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread; tuned;

clarified: consolidated result is last command;

support for anonymous print function values; clarified treatment of retained_prints;

tuned;

store Isabelle symbols in canonical form; tuned signature;

clarified outermost progress.interrupt_handler;

report theory progress via PIDE node status;

merge

more conservative output, avoiding nonstandard feature of E

merged

winding numbers predicate

unused

merged

more node status information;

tuned signature;

tuned signature;

shutdown ML process before output: Theories_Result is timeless/stateless;

more operations; more output;

more accurate dependencies; tuned;

tuned;

more formal dump aspects; support output dir;

more operations (as in ML);

clarified option -O: avoid conflict with build/dump option -D;

slicker proof

canonical names

merged

more general tidying

merged

support to dump build database produced by PIDE session;

more accurate theory_graph: avoid imports of loaded_theories with incomplete node name;

clarified signature: Known.theories retains Document.Node.Entry (with header);

clarified signature;

tuned signature;

merged

tidying up a bit more

prefer existing operation;

retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;

clarified signature -- avoid confusion with Resources.is_hidden;

markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);

merged

tidying and reorganisation around Cauchy Integral Theorem

export sort algebra;

tuned;

tuned;

support 'export_files' in session ROOT;

clarified output;

support multiple patterns;

clarified cache;

tuned signature;

tuned output;

merged

merged

tidied some proofs

merged

merged

more small tidying

merged

macOS build: exclude HOL-Proofs

tuned;

merged

added command 'ML_export';

more examples;

tuned output;

pretty-print according to defaults of input syntax;

more accurate diagram;

proper output;

treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd

merged

setup server directory for Cygwin quasi-mirror;

more scalable JVM memory management;

tuned output;

more general cache, also for term substructures;

more exports; read_session: proper signature;

generalized Cramer's rule

tuned

reorganization, everything based on Tree2 now

avoid overaggressive classical rule

By Andrei Popescu based on an initial version by Kasper F. Brandt

merged

small tidy-up of Complex_Transcendental

merged

small clean-up of Complex_Analysis_Basics

more complete and more correct documentation on code generation

grouped material on numeral division

automatic classical rule to derive a dvd b from b mod a = 0

consider dvdE for automated classical proving

added lambda-free HO output for Ehoh (higher-order E prototype)

First step to remove nonstandard "[x <- xs. P]" syntax: only input

merged

removed unicode symbol

Moved Landau_Symbols from the AFP to HOL-Library

merged

more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);

no longer necessary

merged

correcting the statements of the MVTs

one last fix

tidy up of Derivative

avoid undeclared frees;

removed junk;

avoid dangling tfrees;

standardize implicit variables: non-zero indexes do occur occasionally, e.g. via RS;

tuned signature;

avoid undeclared frees;

export facts;

clarified encoding;

more scalable;

tuned output;

more scalable;

tuned;

support HTTPS;

updated to scala-2.12.6;

prefer HTTPS;

override default of Isabelle_Process, notably for PIDE export of "document.tex";

tuned queries;

support for build_database_server (PostgreSQL); clarified signature;