avoid catch-all exception handling;

eliminated fragile catch-all pattern, based on educated guess about the intended exception;

Attribute map_function -> coercion_map; tuned;

syntax category "real" subsumes plain "int";

merged

Plus -> Sum_Type.Plus

Minor reformat.

support for real valued preferences;

support for real valued configuration options;

support for floating-point tokens in outer syntax (coinciding with inner syntax version);

merged

added rule let_mono

CONTRIBUTORS;

more sharing of operations, without aliases;

simplified data lookup;

export declarations by default, to allow other ML packages by-pass concrete syntax; proper Args parsing for attribute syntax (required for proper treatment of morphisms when declarations are moved between contexts); tuned;

proper signature constraint for ML structure; explicit theory setup, which is customary outside Pure; formal @{binding} instead of Binding.name;

proper header; tuned whitespace;

Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).

updated SMT certificates

eta-expand built-in constants; also rewrite partially applied natural number terms

optionally drop assumptions which cannot be preprocessed

added crafted list of SMT built-in constants

clarified error message

tuned

introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list

merged

added listrel1

hide Sum_Type.Plus

merged