abstract algebraic bit operations

more balanced AFP partitioning;

workaround for occasional deadlock seen in HOL-Proofs with threads=2;

adapted to 3869b2400e22;

tuned output;

more options: client without implicit server startup;

console interaction with line-editor;

more flexible message formats;

clarified interrupt handling;

clarified signature;

option for console interaction;

more uniform Bytes.read_line/read_block operations;

auto update;

more comments;

more general TTY loop;

added Reply.NOTE for asynchronous notifications;

more operations;

more thorough init: purge inactive entries;

more generous timeout;

Entry.connection: proview password here; more robust checks;

clarified initial protocol;

ignore empty lines;

tuned;

more robust read_line after shutdown;

more implicit wire protocol;

tuned signature;

clarified server start, notably for invocation within regular Isabelle/Scala process;

tuned signature;

tuned signature;

clarified toString operations;

clarified socket connection;

server commands may access Server; Server.stop: proper shutdown; clarified signature;

tuned -- avoid regex matching on potentially large string; clarified message: command name could be malformed;

more robust build: prevent problems seen with Poly/ML eb94e2820013 on Mac OS X;

clarified notion of unknown files: ignore files outside of a Mercurial repository;

more balanced AFP partitioning;

more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

tuned -- more uniform;

eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

Drop rewrite rule arguments of sublocale and interpretation implementations.

more balanced AFP partitioning;

clarified signature;

build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;

more robust: normalize potentially symbolic rev;

proxy setup for lrzcloud1;

tuned signature;

support for permissive connections, for odd situations where host keys are not accepted;

proper target directory;

eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);

document existing Apache2 configuration;

consolidated main cronjob server on virtual machine together with build_log database; eliminated special tricks for Gentoo; import plain_identify logs, export all logs for backup; run build_release, build_history_base in parallel to remote_build_history tasks;

identify closer to main cronjob -- avoid diverging changeset versions;

Drop rewrites after defines in interpretations.

proper remote_mac according to Admin/Release/CHECKLIST;

more Java heap, e.g. relevant for hg.graph on Isabelle repository;

more robust check -- do not rely on return code;

more compact ML_Statistics, to make build_status work with less than 2GB heap;

retain latest ml_stats (amending e76c6cb0d461);

accomodate smaller build machine;

clarified signature;

clarified self_update: imitate visible directory state on remote side;

more operations;

self_update implies push_isabelle_home (see also 4c253e84ae62);

uniform setup_repository (pull/clone without update); tuned signature;

clarified signature: facilitate interactive experimentation;

clarified tasks;

tuned signature;

proper order;

clarified README;

merged

more ssh options;

support for proxy connection, similar to ProxyCommand in ssh config;

prefer https;

avoid hardwired parameters; less ambitious defaults: low memory requirements;

Drop illegitimate optimisation from d5a7f2c54655.

Fall back to reading rewrite morphism first if activation fails without it.

Proper rewrite morphisms in locale instances.

clarified date for presentation vs. formal pull_date;

reveal raw data in CSV format;

support for CSV files;

tuned comment;

clarified syntax: reject formal comments explicitly, instead of ignoring them silently;

merged

generalized lemmas about orthogonal transformation

more explicit infixl (see initial 1edf0f223c6e); clarified name;

clarified use of vec type syntax;

new lemma

dedicated append function for string literals

generalized

moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

merged

prefer symbols;

tuned;

more abbrevs;

allow multiple entries of and_list (on both sides);

eliminated ASCII syntax from Pure bootstrap; tuned comments;

merged

new material on matrices, etc., and consolidating duplicate results about of_nat

notation for dummy sort;

more symbols;

merged

tuned signature;

tuned signature;

tuned signature;

removed unused clone of (map o apsnd); removed unused variant of HOLogic.mk_obj_eq;

prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS;

added HOLogic.mk_obj_eq convenience and eliminated some clones;

tuned -- use existing Morphism.instantiate_morphism;

Merged;

merged

Unified the order of zeros and poles; improved reasoning around non-essential singularites

merged

tuned;

tuned signature -- eliminated clones;

command 'interpret' no longer exposes resulting theorems as literal facts;

more robust normalization of witness, e.g. relevant for proofs of transfer_existence_ivl0, transfer_flow0 in AFP/thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy;

tuned;

more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;

explicit operations to instantiate frees: typ, term, thm, morphism;

more operations for ctyp, cterm;

minor tuning and clarification;

minor tuning and clarification;

tuned signature;

fixed the proof of pair_measure_count_space

merged

fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring

merged

type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0

simplified Radix_Sort

merged

merged

moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

simplified def of stable

Lots of new material about matrices, etc.

tuned proofs -- prefer explicit names for facts from 'interpret';

merged

eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);

tuned signature;

tuned;

use lazy notes for locale context init and later additions of facts;

avoid premature Lazy.force due to strict "?" operator;

Merge

Merge

lots of new material, ultimately related to measure theory

merged

support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes; register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel); support for lazy notes for locale activation (still inactive);

tuned;

tuned: more parallel;

clarified modules;

clarified modules;

tuned;

tuned;

tuned signature;

tuned: more accurate transfer;

store facts as lazy values;

clarified operations;

misc tuning and clarification;

clarified signature;

clarified modules;

more operations;

added lemma

tuned;

clarified signature;

misc tuning and clarification; removed unused all_registrations_of;

clarified signature;

more explicit instantiate_morphism (without checks for typ / term component);

tuned;

tuned signature;

more thorough jEdit.propertiesChanged(), which includes KeymapManager.reload() and jEdit.initKeyBindings();

avoid conflict with Isabelle/jEdit completion of '>', e.g. "-->", "==>";

trim context of persistent data;

trim context of persistent data;

trim context of persistent data;

clarified apply_transaction: always continue without presentation context;

more tight presentation context: avoid storing full Toplevel.state;

tuned;

more informative theories_trace;

merged

tuned signature (again);

trim context of persistent data;

trim context of persistent data;

proper file name;

trim context of persistent data; tuned signature;

clarified data operations, with trim_context and transfer;

tuned;

trim context of persistent data; tuned;

trim context of persistent data;

removed unused material;

trim context of persistent data;

trim context of persistent data; no need to trim context for del operations;

tuned;

tuned whitespace;

more operations;

optional trace of created theory values;

more operations;

auxiliary operation for space profiling;

special treatment of 0 only refers to type char

merged

features and caveats of datatype_record

merged

strengthen filter relator to canonical categorical definition with better properties

recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;

merged

more symbols;

New theory ex/Radix_Sort.thy

records based on datatypes/BNF infrastructure

updated polyml component;

no --enable-shared: leads to slow bigint operations (e.g. in session HOL-ODE-Examples);

retain remote_builds_old for build_status;

lxbroy7 no longer exists;

added lemmas

corrected some URLs

permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc;

merged

updated polyml component -- omitting bad polyml-5.7.1-3;

use preferred resolver according to DOI Handbook §3.8

no --enable-shared for x86_64-darwin: does not work on some test machine;

proper target directory;

tuned;

more robust options;

back to --disable-shared on windows to avoid odd core-dump of polyimport;

tuned;

back to --disable-shared on x86-darwin to avoid odd core-dump of polyimport;

clarified command-line defaults;

enforce shared libpoly on all platforms, with File.copy before File.move;

NEWS;

updated to polyml-5.7.1-2, which includes libgmp for x86-darwin as well;

support for libgmp for x86-darwin;

more accessible src/Pure/ROOT.ML;

tuned;

more robust: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses);

rebuild of polyml-5.7.1 with libgmp for x86_darwin;

patch polyc: avoid hardwired directory prefix;

support for libgmp for x86_64-darwin;

built-in library path for (optional) libgmp on macos;

removed obsolete polyi executable: change of DYLD_LIBRARY_PATH is not required;

more robust access to shared libraries for poly executable: avoid global change of LD_LIBRARY_PATH (e.g. relevant for subprocesses);

Merged

Some lemmas about complex sinh/cosh/tanh

more elementary proof of connected_Times, earlier