take out remote E-SInE -- it's broken and Geoff says it might take quite a while before he gets to it, plus it's fairly obsolete in the meantime

Moved extraction part of Higman's lemma to separate theory to allow reuse in theories compiled without support for proof terms.

Removed hcentering and vcentering options, since they are not supported by all versions of geometry.

merged

Added documentation for HOL-SPARK

drop partial monomorphic instances in Metis, like in Sledgehammer

better type reconstruction -- prevents ill-instantiations in proof replay

NEWS: mention replacement lemmas for the removed ones in Complete_Lattices

changing quickcheck_timeout to 30 seconds in mutabelle's testing

adding post-processing of terms to narrowing-based Quickcheck

HOL/ex/ROOT.ML: only list BinEx once

merged

remove redundant instantiation ereal :: power

reintroduced Minipick as Nitpick example

tuned comment

merged

Extended_Real_Limits: generalize some lemmas

add lemmas within_empty and tendsto_bot; declare within_UNIV [simp]; tuned some proofs;

made SML/NJ happy;

abstract System_Channel in ML (cf. Scala version); back to TextIO for fifo, which is more stable in Poly/ML 5.4.x; explicit block buffering -- BinIO might be subject to old Poly/ML defaults;

alternative Socket_Channel; use BinIO for fifos uniformly;

more abstract wrapping of fifos as System_Channel;

slightly more general Socket_IO as part of Pure;

more hints on Z3 configuration;

reduced default thread stack, to increase the success rate especially on Windows (NB: the actor worker farm tends to produce 100-200 threads for big sessions);

renamed inv -> filter

Added proofs about narowing

added missing makefile dependence

added example

tuned