Use interpretation in locales.

new examples

*** empty log message ***

new command to invoke ATPs

small mods to code lemmas

made SML/XL happy;

list_all_conv -> iff

name fix

added quite a few functions for code generation

more simprules now have names

classical rules must have names for ATP integration

added listT

support for document versions;

eliminated datatype token; replaced output_tokens by separate output_XXX; replaced flag_markup by markup_true/false; added begin/end_delim, begin/end_tag;

begin_index: list of docs;

added eq_syntax;

export proof_syntax, proof_of;

added String.isSuffix;

state: body context; added theory_context, proof_to_theory_context; added is_proof, level; turned excursion_result into present_excursion;

P.tags;

use_dir: removed hidden, added doc_versions;

back: removed ill-defined '!' option;

added transfer; adapt local syntax to potential changes of theory syntax; added pretty_proof(_of);

moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML); support for tagged commands; tuned theory presentation interface;

added tags parser;

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;