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

refined comment

fixed two typos in IMP (by Jean Pichon)

merged