improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position;

removed unused Toplevel.properties;

added combinator for wrapped lazy evaluation;

added setmp_thread_data_seq;

removed obsolete context_position.ML (superseded by Position.thread_data);

switched to polyml-cvs;

Reimplemented proof of strong induction theorem.

Added lemma at_fin_set_fresh.

reactivated mk of java/scala sources, with paranoia PATH setting for sunbroy;

exceptions: assign result = null properly;

tuned proofs;

recovered #der example without using val it;

yet another OCaml fix

tuned

added map_split

added class semiring_div

fixed OCaml

avoid 'it' in ML expressions

Removed Logic.auto_rename.

Efficient_Nat streamlined and improved

tuned proof

non-negative numerals

tuned

more lemmas

proper meaningful examples

explicit auxiliary function for code setup

streamlined and improved

adjusted to constant and theorem renames

avoiding direct references to numeral presentation

tuned code setup

add space to binder syntax

pcpodef generates strict_iff lemmas