tuned signature;

tuned signature;

clarified signature: support meaningful subclasses for Build.Engine implementations;

support alternative build engines, via system option "build_engine";

misc tuning and clarification; support SSH.System;

proper test, following Platform.is_linux;

clarified signature;

clarified signature;

merged

Simplified some more proofs

merged

Replacing z powr of_int i by z powi i and adding new material from the AFP

merged

tuned: avoid redundant white space;

clarified signature: more robust operations, without assumption about node 0;

clarified signature: more concise operations;

clarified modules: NUMA is managed by Build_Process;

tuned signature;

clarified signature: move all parameters into Build_Process.Context;

clarified signature;

more elementary data structures, to fit better to SQL database;

clarified signature (see also 68a7ad1385bc);

clarified signature;

clarified modules; clarified signature;

merged

merge in backouts

Backed out changeset bafdc56654cf

backout rev 334015f9098e (for Main_Doc.thy only)

Backed out changeset 1fde0e4fd791

merged

Simplifying more proofs

merged

proper Nodes.init (amending 9b35c1171d9a);

unused;

tuned;

clarified signature defaults;

clarified types: support a variety of Build_Job instances;

clarified signature: more explicit synchronized operations;

clarified signature: more explicit synchronized operations;

clarified modules (again); clarified signature: idempotent "finish" operation, analogous to "join";

clarified signature: more explicit synchronized operations;

clarified signature: more explicit synchronized operations;

more robust: first register job, then start job;

clarified signature: proper scope of synchronized operation;

proper synchronized access to mutable state, to support concurrency eventually;

tuned signature: explicit marker for mutable global state;

tuned;

more robust;

clarified signature;

clarified modules;

merged

Tidied some really messy proofs

added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO

Simplified a few proofs

Moved up a theorem

Limit properties for complex exponential

More of Eberl's contributions: memomorphic functions

merged

New material due to Eberl on Formal Laurent Series

merged

A bit more tidying and some new material

removed rarely used error in Sledgehammer

merged

tuned

added refute mode to Sledgehammer to find 'counterexamples'

merged

Map.map_of movement

removed Map from docu

move map_of to List

updated NEWS

careful eta-contraction in Metis to keep argument to All and Ex expanded

merged

merged

clarified main operations; clarified main loop;

clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;

prefer global mutable state, in order to break up the loop eventually;

clarified modules;

clarified signature;

clarified static build_context vs. dynamic queue;

clarified signature: make dynamic Queue from static Context;

clarified data structure: absorb Option[Process_Result] into Process_Result, e.g. to simplify database storage;

tuned;

tuned;

clarified data structure: use static info from deps, not dynamic results; tuned;

clarified data structure: more direct access to timeout;

tuned;

misc tuning and clarification;

clarified modules; clarified signature;

tuned message: old_time not sufficiently prominent nor accurate to be printed;

clarified signature and terminology;

clarified signature: avoid adhoc constants;

tuned;

tuned message;

tuned signature: more operations;

clarified signature: more explicit types;

clarified modules;

clarified signature;

clarified signature;

merged

Simplification of proofs

explicit range types in abstractions

somehow more clear terminology

tuned

Some basis results about trigonometric functions

merged

Even more new material from Eberl and Li

merged

More material for Analysis and Complex_Analysis

actually executable enum_all, enum_ex for word

tuned text

Lots of new material chiefly about complex analysis

merged

More new theorems from the number theory development

merged

proper orientation for right-associative operations;

tuned signature;

tuned signature;

tuned signature;

obsolete --- superseded by SHA1.Shasum operations;

clarified signature, using right-associative operation;