minor tuning for release;

source files are always encoded as UTF-8;

eliminated fragile HTML.with_charset -- always use utf-8;

recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;

removed old generated stuff; removed DOS line endings;

comment;

update documentation

replace "smt" prover with specific SMT solvers, e.g. "z3" -- whatever the SMT module gives us

export more information about available SMT solvers

setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;

use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."

updated generated file;

removed confusing comments (cf. 500171e7aa59);

merged

removed outdated lint script

merged

compile

run synchronous Auto Tools in parallel

really fixed comment (cf. 7abeb749ae99)

theorem names generated by the (rep_)datatype command now have mandatory qualifiers

eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended

NEWS

only instantiate type variable if there exists some in quickcheck

fixing comment in library

adapting predicate_compile_quickcheck

adding a nice definition of Id_on for quickcheck and nitpick

adding code equation for finiteness of finite types

improving sledgehammer_tactic and adding relevance filtering to the tactic

adapting mutabelle

adapting SML_Quickcheck to recent changes

explaining quickcheck testers in the documentation

adapting quickcheck examples