use theory instead of obsolete Sign.sg; tuned comments;

added map_specs/facts operators (from locale.ML);

removed obsolete Theory.sign_of;

load method.ML before proof.ML;

added interfaces for compile translation functions (from Isar/isar_thy.ML);

added tap;

updated;

usedir: tuned option -V;

usedir: removed option -H;

* Proper output of proof terms within a proof context; * Proper output of antiquotations for theory commands involving a proof context; * 'print_theorems': in theory mode print difference of facts, in proof mode print local facts;

Improved generation of witnesses in interpretation.

Interpretation in locales.

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;