more intimate definition of fold_list / fold_once in terms of fold

canonical fold signature

formal notepad without any result;

added Syntax.default_root; simplified Syntax.parse operations; clarified treatment of syntax root for translation rules -- refrain from logical_type replacement; tuned error message;

eliminated obsolete Token.Malformed -- subsumed by Token.Error;

tuned @{datatype} using Syntax.pretty_priority (NB: postfix type application yields Syntax.max_pri, so arguments in prefix application require higher priority);

added Syntax.pretty_priority;

merged

conventional point-free characterization of rsp_fold

replaced memb by existing List.member

explicit type constraint; streamlined notation

tuned proposition

lemma multiset_of_rev

lemmas fold_remove1_split and fold_multiset_equiv

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