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;