tuned the proof of the substitution lemma

rename_client_map_tac: avoid ill-defined thm reference;

use_thy: do not set implicit ML context anymore;

added ambiguity_limit (restricts parse trees / terms printed in messages); tuned;

renamed thms_containing_limit to FindTheorems.limit;

eliminated some legacy ML files;

added bind_thms;

tuned;

removed legacy ML file;

syntax error: unified output of priorities;

syntax error: reduced spam -- print expected nonterminals instead of terminals; tuned pretty_gram;

avoid redundant escaping of Isabelle symbols;

grouped versions of axioms/define/notes;

misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion;

added theorem group property;

added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name;

added surround;

tuned attribute syntax -- no need for eta-expansion;

added theorem group;

internal inductive: fresh theorem group;

modernized primrec;

Codegenerator vs. Codegenerator_Pretty: loaded sequentially, due to hazardous ML sections; more simultaneous use_thys;

modernized primrec;

tuned document; modernized primrec;

tuned document;

tuned;

* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here;

tuned

print postprocessor equations

fixed and tuned

dropped superfluous code theorems

improved code theorem setup

consistent interacitve bootstrap of HOL-Main

distinguished examples for Efficient_Nat.thy

clarified setup of method "normalization"

moved definition of power on ints to theory Int

removed unused properties; replaced ContextPosition by Position.thread_data;

replaced ContextPosition by Position.thread_data;

statement: keep explicit position; replaced ContextPosition by Position.thread_data;

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