clarify is_newline vs. is_blank; removed is_indent; added is_comment;

default tags for theory/proof/ML commands; added '%' keyword;

reimplemented theory presentation, with support for tagged command regions; tuned antiquotation output;

back: removed ill-defined '!' option; print_theorems: print facts in proof mode; print_prfs: proper context version -- ProofContext.pretty_proof_of;

replaced sign by thy;

added liberal_name;

tuned Symbol.spaces;

tuned Buffer.add;

tuned unsuffix/unprefix;

type proof: theory_ref instead of theory (make proof contexts independent entities); added transfer_proof;

Isar command keyword classification (from Isar/outer_syntax.ML);

added Isar/outer_keyword.ML;

OuterKeyword;

updated;

removed -H false;

isatool usedir: option -V and -f; isatool document: option -n and -t;

tuned antiquotations; added tagged commands;

\isabellestyleit: proper \isacharbackslash; support for tagged regions: \isakeeptag, \isadroptag, \isafoldtag -- depends on plain TeX version of comment.sty;

proper ML_DBASE for .../bin/poly;

added option -V VERSION; removed option -H;

added option -n NAME and -t TAGS;

-V outline=/proof,/ML;

* Command tags control specific markup of certain regions of text (replaces usedir -H);

simp_depth warning now mod 20, not mod 10 (too often)

lucas - added pretty printing function and cleaned up signature a little.

lucas - fixed bug in changing focus - when moving up and right, if an abs was encountered it would move up an extra time. I also removed the spurious pretty printing function that did nothing.

New command: interpretation in locales.

moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy

exported after_qed for arity proofs

added finite(option) to Recdef.thy