merged

Backed out changeset 1fde0e4fd791

merge in backouts

backout rev 334015f9098e (for Main_Doc.thy only)

Backed out changeset bafdc56654cf

tuned metis call to avoid obscure feature

merged

Simplifying more proofs

unused;

proper Nodes.init (amending 9b35c1171d9a);

merged

tuned;

clarified signature defaults;

clarified types: support a variety of Build_Job instances;

clarified signature: more explicit synchronized operations;

clarified modules (again);

clarified signature: more explicit synchronized operations;

clarified signature: more explicit synchronized operations;

clarified signature: more explicit synchronized operations;

clarified signature: proper scope of synchronized operation;

more robust: first register job, then start job;

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

merged

Migration of material to the repository and necessary modifications

Limit properties for complex exponential

More of Eberl's contributions: memomorphic functions

New material due to Eberl on Formal Laurent Series

merged

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'

more map_of adaptions

adapted to new List.map_of

Map.map_of movement

merged

removed Map from docu

move map_of to List

updated NEWS

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

update Real_Time_Deque

Removal of a stray sledgehammer command

merged

merged

clarified signature: prefer stateful object-oriented style, to make it fit…

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

clarified main operations;

clarified signature;

clarified modules;

clarified static build_context vs. dynamic queue;

clarified signature: make dynamic Queue from static Context;

tuned;

tuned;

clarified data structure: absorb Option[Process_Result] into Process_Result, e.

clarified data structure: more direct access to timeout;

misc tuning and clarification;

tuned;

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

clarified modules;

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

clarified signature and terminology;

clarified signature: avoid adhoc constants;

tuned;

tuned message;

clarified signature: more explicit types;

tuned signature: more operations;

clarified modules;

clarified signature;

clarified signature;

merged

Simplification of proofs

explicit range types in abstractions

tuned

somehow more clear terminology

explicit range types in abstractions

somehow more clear terminology

merged

Some tidying and moving some material to the distribution

Some basis results about trigonometric functions

Deleted use of Euclidean_Division

Repaired session name

"Repaired boundary behaviour of mod+- for even modulus, Added locale…

merged

Even more new material from Eberl and Li