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);