mksimps and mk_eq_True no longer raise THM exception.

Added label for section on terms.

Added documentation for proof terms.

Added TYPE to Pure grammar.

Added \ttlbrack and \ttrbrack.

Added TPHOLs2000 paper about proof terms.

updated;

tuned;

tuned;

- Exchanged % and %%. - Fixed bug in shrink.

- Tuned syntax - proof_of_term: fixed problems with dummy patterns and typing information

- Exchanged % and %% - Renamed reconstruct_prf to reconstruct_proof

Exchanged % and %%.

HOL: eliminated global items;

updated;

eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");

renamed theory "subset" to "Typedef";

unsymbolize;

renamed "()" to Unity;

HOLogic.unit;

made unit type local;

tuned:

renamed "()" to Unity, made local;

added surjE;

prepared for Isabelle2001;

renamed real_of_nat_eq_cancel to real_of_nat_inject, and declared as iff rule;

updated;

renamed real_of_int_eq_iff to real_of_int_inject;

document setup;

new-style theory;

Square roots of primes are irrational;

AddXIs [dvdI]; AddXEs [dvdE]; added dvd_mult_div_cancel;

tuned;

tuned;

tuned;

AddXEs [UnI1, UnI2];

AddXEs [disjI1, disjI2];

ex/Hilbert_Classical.thy ex/document/root.tex;

tuned;

document setup;

derive tertium-non-datur by means of Hilbert's choice operator;

obsolete;

updated;

-v option;

verbose option;

use_dir: verbose option;

removed option -d (now standard behaviour); added option -q; include notes;

option -v;

activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;

updated;

tuned order;

bold symbols;

tuned;

turn bullet into bold cdot (looks much better in printed output);

use darkblue for all links;

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

cosmetics

Final version of Florian Kammueller's examples

new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted

improved version of the Pi-theorems

PiSets moved to GroupTheory, while LocaleGroup deleted

live links

The final version of Florian Kammueller's proofs

slight improvement for iff attribute

replaced SOME by THE;

the_equality [intro];

tuned;

declare trans [trans] (*overridden in theory Calculation*);

HOL: added "The";

private "myinv" (uses "The" instead of "Eps");

replaced "Eps" by "The";

HOL_ss: the_eq_trivial, the_sym_eq_trivial;

tuned;

added "The" (definite description operator) (by Larry);

*** empty log message ***

SEDINDEX = ./isa-index;

tidying the index

tidying the index

indexing

abtract non-emptiness statements (no longer use Eps); cleaned up;

tuned;

working

oops

fixed bad error in tdxbold; also removed default indexing in \\rulename

tweaks

added\\protect

more indexing

indexing tweaks

less indexing of theorem names

indexing

contrapos_pn

index file

removed a4paper

more in the Springer style

indexing

indexing

messages, and proper treatment of footnotes

new preface

tweaks for new version

indexing and tweaks

tweak

careful changes to make its output identical to that of indexing macros

new macro file for the tutorial

separate preface and macro file

do not remove Rules and Sets TeX files