local coercion insertion algorithm to support complex coercions

printing and deleting of coercions

raw unbuffered socket IO, which bypasses the fragile BinIO layer in Poly/ML 5.4.x;

default print mode for Isabelle/Scala, not just Isabelle/jEdit;

augment existing print mode;

explicit option for socket vs. fifo communication;

tuned proof;

synchronized section names with manual

merged;

discontinued legacy theorem names from RealDef.thy

merged

discontinued HOLCF legacy theorem names

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