tuned some proofs;

removed obsolete arities;

tuned size of included graph;

added \isachardoublequoteopen/close, \isacharbackquoteopen/close;

(branch cleanup)

(allocating new branch)

added superclasses, class_le_path

added alist.ML

added 'these', removed assoc2

added alist module

Fixed bug.

DFG output now works for untyped rules (ML "ResClause.untyped();")

Lemmas on dvd, power and finite summation added or strengthened.

replaced '?' by '??'

Adapted to new code generator syntax.

Put quotation marks around some occurrences of "file", since it is now a reserved keyword.

Adapted to new code generator syntax.

Implemented incremental code generation.

fixed typo

add_locale_context(_i) now exporting elements (still some refinements to be done)

added ? combinator for conditional transformations

added 'default' function

Printing of interpretations: option to show witness theorems;

Interpretation in locales: extended back end; Printing of interpretations: option to show witness theorems;

replaced ? by ??

fixed deps;

tuned arrangement of generated stuff;

updated;

tuned generated stuff;

updated;

updated;

obsolete;

tuned;

updated;

*** empty log message ***

updated;

updated;

-H deleted

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;