Deleted unnecessary rules

fixed font names;

exit_use_dir; tuning;

isatool usedir;

exit_use_dir;

remove empty dirs;

isatool usedir;

improved session names;

isatool usedir;

*** empty log message ***

tuned;

isatool usedir;

exit_use_dir;

isatool usedir;

replaced ex.ML by ex/ROOT.ML, ex/ex.ML;

isatool usedir;

added ex dir;

replaced ex.ML by ex/ROOT.ML, ex/ex.ML;

replaced ex.ML by ex/ROOT.ml, ex/ex.ML;

Improved intersection rule InterI: now truly safe, since the unsafeness is delegated to exI.

delete_tagged_brl just ignores non-elimination rules instead of complaining

delrules now deletes ALL occurrences of a rule, since it may appear in any of the four lists.

added quit();

asserts $ISABELLE_OUTPUT_DIR;

Added wp_while.

added dummy set_session;

usedir -- build object-logic or run examples;

A more explicit prefix because gensym now generates easily predicatable identifiers

gensym no longer generates random identifiers, but just enumerates them starting from A. The random number generator was needlessly slow and caused portability problems.

Made the indentation rational

fixed Tools path;

Conducted the IFOL proofs using intuitionistic tools

Stopped giving Introduction rules as Elimination rules

Added P&P&Q <-> P&Q and P|P|Q <-> P|Q

Added P&P&Q = P&Q and P|P|Q = P|Q.

*** empty log message ***

The HOLCF-based den. sem. of IMP.

Added the HOLCF-based den. sem. of IMP.

Added link to HOLCF/IMP

fixed perl path;

uncommented chown / chmod (again);

Modified proofs because simplifier does not eta-contract any longer.

Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.

tuned glyphs;

tuned Sigma glyph;

major tuning;

tuned comments; added -h option;

tuned comments; added ISABELLE_TOOLS support;

tuned comments;

tuned;

tuned comment; more robust check;

Note on fonts and remote X11;

tr is (again) type abbrev;

added THIS_IS_ISABELLE_BUILD;

added THIS_IS_ISABELLE_BUILD discrimination;

The contr_tac, which replaces a fast_tac, is needed only because eq_assume_tac does not recognize eta-equality. But making it do so is costly

renamed;

fixed;

commented out chwon, chmod;

fixed src path;

added \n at EOF;

*** empty log message ***

tuned;

renamed fonts;

renamed font;

removed lparr, rparr, empty, succeq, ge, rrightarrow; added turnstile, Turnstile, cdot, approx, Colon, bow; renamed tick to surd;

renamed SYSTEM to RAW_ML_SYSTEM;

added \<Colon> syntax for constraints (more compact!);

"bool lift" now syntax instead of type abbrev;

*** empty log message ***

added atac 2 (again);

removed (| |) symbols syntax;

fixed Not syntax;

tuned comment;

tuned comments;

Isabelle installation notes;

now sans serifs;

tuned;

*** empty log message ***

build - compile parts of the Isabelle system;

moved settings comment to build;

Removed some polymorphic equality tests

Improved indentation of aconv

Corrected aeconv and exported it

Prevent permutation of assumptions in hyp_subst_tac

Deleted steps made redundant by the stronger eq_assume_tac

Eta-expanded some declarations for compatibility with value polymorphism

Tidied and updated

more robust check;

renamed, improved, augmented version of isabelle fonts;

tuned comment;

tuned;

pass xterm mode by default;

Minor changes due to primrec definition for ^

primrec definition for ^

Minor changes due to primrec definition for nth