*** empty log message ***

initial setup for chapter on document preparation;

updated output;

- declared wf_java_prog as syntax (previously: definition) - in wf_java_mdecl: added preconditions for 'This' - rule LAss: precondition v ~=This

Removed some unfoldings of defs after declaring wf_java_prog as syntax

Added axiom e~=This to reflect strengthened precond. in rule LAss

Minor modifications

added Ordinals example;

Tuned indentation of abstractions.

tuned;

inductive: no collective atts;

inductive: no collective atts;

oops;

tuned;

recdef (permissive); inductive: no collective atts;

*** empty log message ***

prove: ``strict'' argument;

internal thm numbering with ":" instead of "_";

avoid handle _;

permissive option;

inductive: no collective atts;

updated;

recdef (permissive);

Tuned section about parsing and printing proof terms.

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];