* Pure/Isar: unified specification syntax admits type inference and dummy patterns; print mode: no_abbrevs;

read/check_specification: free_dummy_patterns;

added free_dummy_patterns;

added minimize_sort, complete_sort;

Sign.minimize/complete_sort;

convenient obtain rule for sets

added code lemma for 1

moved Finite_Set before Datatype

adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);

Attrib.eval_thms; Syntax.parse/check;

Attrib.eval_thms;

read/check_specification: proper type inference across multiple sections, result is in closed form; added read/check_free_specification for single section, non-closed form;

added eval_thms;

minimal adaptions for Specification.read/check_specification;

proper Specification.read_specification; Attrib.eval_thms;

removed dead code;

declare_constraints: declare (fix) type variables within constraints, but not terms themselves;

made SML/NJ happy

rudimentary support for Haskell

added support for Haskell, OCaml

Efficient_Nat and Pretty_Int integrated with ML_Int

proper Sign operations instead of Theory aliases; tuned functor application;

tuned functor application;

proper Sign operations instead of Theory aliases;

simplified interpretation setup;

size hook

removed redundant global_parse operations; renamed global_XXX to XXX_global;

Syntax.parse/check/read; no export of read/cert_axm;

Syntax.parse/check/read;

* Pure/Syntax: generic interfaces for parsing and type checking; tuned;