* Delimiters of outer tokens now produce separate LaTeX macros; * isatool usedir: option -C (default true) controls copying of document directory;

introduced AList.*

better map_entry

fixed bug in record_type_abbr_tr'

patterns in setsum and setprod

Updated import.

updated;

delimiter markup for verbatim tokens;

clarify type tok, do not emit markup flag for suppressed tokens;

use AList operations;

cover tagged command regions; tuned;

tune spacing where a generated theory text is included directly;

updated;

recover original definitions of \isactrlsub etc.;

canonical interface for 'default'

output \<^loc> as 'loc' span; tuned;

isatool latex -o sty;

added 'loc';

updated;

ASCII back-quote no longer sym char;

added \isactrlloc;

* ML functions legacy_bindings and use_legacy_bindings;

avoid symbolic identifier;

added (use_)legacy_bindings;

output_basic: handle AltString token;

removed obsolete type_syn;

unskolem local vars;

tuned;

added alt_string;

added AltString token (delimited by ASCII back-quotes); ASCII back-quote no longer symbolic char;

removed unused dest operation;

export theorems_of;

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;