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;

tuned Symbol.spaces;

tuned Buffer.add;

tuned unsuffix/unprefix;

type proof: theory_ref instead of theory (make proof contexts independent entities); added transfer_proof;

Isar command keyword classification (from Isar/outer_syntax.ML);

added Isar/outer_keyword.ML;

OuterKeyword;

updated;

removed -H false;

isatool usedir: option -V and -f; isatool document: option -n and -t;

tuned antiquotations; added tagged commands;

\isabellestyleit: proper \isacharbackslash; support for tagged regions: \isakeeptag, \isadroptag, \isafoldtag -- depends on plain TeX version of comment.sty;

proper ML_DBASE for .../bin/poly;

added option -V VERSION; removed option -H;

added option -n NAME and -t TAGS;

-V outline=/proof,/ML;

* Command tags control specific markup of certain regions of text (replaces usedir -H);

simp_depth warning now mod 20, not mod 10 (too often)

lucas - added pretty printing function and cleaned up signature a little.

lucas - fixed bug in changing focus - when moving up and right, if an abs was encountered it would move up an extra time. I also removed the spurious pretty printing function that did nothing.

New command: interpretation in locales.

moved wf_induct_rule from PreList.thy to Wellfounded_Recursion.thy

exported after_qed for arity proofs

added finite(option) to Recdef.thy

added selectors 'classes_of' and 'classes_arities_of'

exported dest_def

added 'the_const_constraint'

(added to repository)