ML_idf -> ML

nicer list of axioms used

no need for TPTP2X unless SPASS is used

optimization to incr_indexes?

tuned;

fixed command prompt (was broken due to P.tags);

* The ML antiquotation prints type-checked ML expressions verbatim.

replace freeze by 'setmp show_question_marks false';

proof_to_theory_context: interaction flag;

accomodate interface Proof vs. Method;

added NO_CASES;

moved after method.ML; moved FINDGOAL/HEADGOAL to method.ML; moved type method to method.ML; prepare attributes here; tuned various interfaces (cf. isar_thy.ML); tuned;

prepare attributes here; tuned;

moved before proof.ML; added FINDGOAL/HEADGOAL (from proof.ML); added type method (from proof.ML); moved proof refinement etc. to proof.ML; tuned;

added add_locale_context(_i), which returns the body context for presentation; note_thmss(_i), add_thmss: returns context for presentation; removed map_attrib_specs/facts (cf. Attrib.map_specs/facts);

moved translation functions to Pure/sign.ML; moved attribute preparation to actual operations in proof.ML etc.; removed various trivial interfaces;

various Toplevel.theory_context commands: proper presentation in context; simplified interfaces Proof vs. IsarThy;

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;

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;

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;