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)

(added to repository)

After_qed takes result argument.

Release of interpretation in locale.

fixed typo in ratadd

added hint for position of aqu options in connection with styles

clarified ML_idf

moved some rat functions to library.ML

added more rat functions

Tuned comment.

new lemma

Added ENTCS 2000 paper by Aleksey Nogin.

New case study: pigeonhole principle.

Added Extraction/Pigeonhole.

added Brian Hufmann's finite instances

Fixed bug in code generator for let and split leading to ill-formed code.

Adapted to new argument format of MinProof constructor.

Adapted to new interface og thms_of_proof / axms_of_proof.

Adapted to new interface of thms_of_proof.

- Tuned handling of oracles - Put arguments of axms_of_proof and thms_of_proof into "canonical order"

mentioned change to exp_ge_add_one_self, new transitivity rules

changes from renaming of exp_ge_add_one_self

renamed exp_ge_add_one_self to exp_ge_add_one_self_aux

renamed exp_ge_add_one_self2 to exp_ge_add_one_self

added extra transitivity rules

added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint

changed reference to Lfp.lfp to FixedPint.lfp, ditto for gfp

import FixedPoint instead of Gfp

removed Gfp

removed Lfp

combined Lfp and Gfp to FixedPoint

tuned ML_OPTIONS;

export clear_ss;

added unfold_tac (Simplifier.inherit_bounds);

simprocs: Simplifier.inherit_bounds;

tuned;

First version of interpretation in locales. Not yet fully functional.

Turned simp_implies into binary operator.

Added filter lemma

* Pure/Simplifier: improved handling of bound variables;

determine Poly/ML runtime system version

obsolete;

determine Poly/ML's idea of current hardware and operating system type;

tuned;

Thm.full_prop_of;

Compress.term;

removed atless (use term_ord instead); removed (inefficient) insert_aterm; improved bound: nameless, avoid allocating new strings; tuned sort_ord/typ_ord: dict_ord; tuned abstract_over: SAME; tuned add_term_vars/frees: OrdList.insert; removed compress_type/compress_type (cf. compress.ML);

export MataSimplifier.inherit_bounds;

Compress.typ;

Compress.init_data;

nameless Term.bound;

improved bounds: nameless Term.bound, recover names for output;

tuned dict_ord;

replaced atless by term_ord;

chain_history: turned into runtime flag; added monomorphic; removed (inefficient) fast_overloading_info; Compress.typ; tuned;

compression of terms and types by sharing common subtrees;

added compress.ML;