tuned proofs;

removed obsolete name_of -- cf. decode;

desymbolize: use Symbol.decode directly; recovered coding conventions of this file;

try SAT_Examples last, to minimize impact of global side-effects;

home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);

Inserted missing theory dependency

merged

Merged.

Removed obsolete code.

updated to official Poly/ML 5.3.0;

switched some isatest sessions to official Poly/ML 5.3.0;

setup for official Poly/ML 5.3.0, which is now the default;

locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;

eliminated hard tabulators;

fixed some inappropriate names

merged

New theory Probability/Borel.thy, and some associated lemmas

merged

tuned error messages; tuned code

follow standard theory merge behaviour: do not change already selected solver

generalized proof by abstraction, abstract propositional nnf goals (lets best_tac succeed on very large terms)

made theory merge deterministic wrt. the selected solver

merged

merged

Repaired handling of comprehensions in "values" command.

updated functor Theory_Data, Proof_Data, Generic_Data;

modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;

adapted Theory_Data; tuned;

adapted Theory_Data; handle Symtab.DUP during actual merge;

tuned;