updated;

updated;

*** empty log message ***

tuned;

Minor improvements, added Example

tuned;

Fixed proof term bug in permute_prems.

result_error_default: include msg;

*** empty log message ***

marginally improved comments

corrected antiquotations in comment

simplified vnam/vname, introduced fname, improved comments

tuned usage;

print_state: subgoals;

export pretty_goals;

result_error_default: output *single* error message;

tuned;

ISABELLE_INTERFACE=none by default (cannot expect X11 everywhere);

* system: support Poly/ML 4.1.1 (large heaps); * system: smart selection of Isabelle process versus Isabelle interface, accomodates case-insensitive file systems (e.g. HFS+);

smart selection of isabelle-process versus isabelle-interface;

renamed "antecedent" case to "rule_context";

*** empty log message ***

*** empty log message ***

tuned;

final proofs := 0;

HOL-Real-Hyperreal made a plain session (no longer an image);

renamed `keep_derivs' to `proofs', and made an integer;

* Proof General keywords specification is now part of the Isabelle distribution (see etc/isar-keywords.el);

proper use of invent_names;

fixed header;

tuned headers;

keyword classification tables for Isabelle/Isar Proof General (generated by ProofGeneral.write_keywords from Isabelle/HOLCF/IOA);

New code generators for HOL.

Initial revision of tools for proof terms.

Added new option for setting level of detail for proof objects.

Proof of True_implies_equals is stored with "open" derivation to facilitate simplification of proof terms.

Added code generator setup.

Added new files for code generator.

Renamed functions % and %% to avoid clash with syntax for proof terms.

Adapted to new proof terms.

Exported ml_reserved.

Made consts list operations a bit faster.

Added new argument to use_dir for derivation kind.

Removed tag_assumption.

Tuned naming of theorems.

Added functions for printing primitive proof terms.

Tuned function extend_lexicon.

Initial revision of tools for proof terms.

Now obsolete; replaced by LF style proof terms.

Initial version of generic code generator.

New implementation of LF style proof terms.

Replaced old derivations by proof terms.

Tidied function SELECT_GOAL.

Added equality axioms and initialization of proof term package.

Added setup for code generator.

Added function unique_strings.

- exported SAME exception - exported functions for normalizing types

Some basic rules are now stored with "open" derivations, to facilitate simplification of proof terms.

Added new files for proof terms.

generated by Session.name;

export name;

cosmetics

removed imname, uncurried Meth

avoid ML bindings;

Implemented indentation schema for conditional rewrite trace.

Traced depth of conditional rewriting

tuned error message;

prefer immediate monos; tuned;

support for absolute namespace entry paths;

Updated proofs to take advantage of additional theorems proved by "typedef"

removed obsolete "arities";

tuned;

corrected initialization of locals, streamlined Impl

corrected semantics of [iff] concerning rules with premises

replaced 1 by 1'

revisions and indexing

added pair_imageI (also as intro rule)

renamed addaltern to addafter, addSaltern to addSafter

added constify_ast_tr;

field_name_ast_tr superceded by constify_ast_tr in Pure;

_constify;

constify numeral tokens in order to allow translations;

* HOL: syntax translations now work properly with numerals and records expressions;

layout, subscripts

[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";

polyml-4.1.1;

Hilbert_Choice is needed only in Main itself

Main is the proper parent of IOA

get it working again using Hilbert_Choice

Getting it working again with 1' instead of 1

new ZF/UNITY theory

*** empty log message ***

changed to full expressions with side effects

changed to full expressions with side effects

tuned;

tuned;

fix problem with user translations by making field names appear as consts;

tuned;

- Fixed bug in isomorphism proofs (caused by migration from SOME to THE) - Funs_rangeE now requires function g to be injective

Eliminated dependency of Funs_rangeE on SOME.

removed the warning from [iff]

Tweaks for 1 -> 1'

Converted 1 to 1'

1 -> 1'

Changed 1 to 1' (= Suc 0)

turned translation for 1::nat into def. introduced 1' and replaced most occurrences of 1 by 1'.

three new theorems

removed the warning from [iff]

removed an unsuitable default simprule

tidying and moving the theorem "choice"

new result comp_surj

numerous stylistic changes and indexing

additional revisions to chapters 1, 2

revisions and indexing

defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some dynamically, so recdef no longer needs to import Hilbert_Choice.

Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice

partial restructuring to reduce dependence on Axiom of Choice

removed reference to Ex_def

partial restructuring to reduce dependence on Axiom of Choice

tweaks and indexing