remove cl.cam font server;

exec the emacs;

Base theory is now Arith, not Nat. (because all datatypes now require Arith).

All datatypes now require Arith.

Added overloaded function `size' for all datatypes.

exhaust_tac can now deal with whole terms rather than just variables.

added href to Isamode;

fixed doc;

adapted to Isamode 2.6;

tuned Isamode stuff;

New headers and other minor changes

Now the recdef induction rule variables are named u, v, ...

New example of recdef and permutative rewriting

Now uses type option instead of Fail/Subst No references to wf_rel_prod

Now uses type option instead of Fail/Subst

Uses option_case_tac

Deleted rprod: lex_prod is (usually?) enough

Deleted obsolete proofs. But option_case_tac will be obsolete too

New example: ex/Fib

New lemmas used for ex/Fib

Added rotation to exhaust_tac.

tuned;

added;

tuned;

SYNC;

Documented exhaust_tac.

fixed packages;

fixed packages;

tuned comments;

Replaced res_inst-list_cases by generic exhaust_tac.

Added exhaustion thm and exhaust_tac for each datatype.

fixed find cmd;

set version;

tuned all READMEs;

release version (sort of);

SYNC;

fixed spelling;

changes for release 94-8

tuned;

Code tidying: removal of C combinator

Basis library input/output primitives; \!simpset instead of HOL_ss

Basis library input/output primitives; currying the induction rule; removing & from the induction rule

TFL induction rule is now curried

Function "sum" now defined using primrec

Mostly cosmetic changes: updated headers, ID lines, etc.

Removed rprod from the WF relation

Removed rprod from the WF relation; simplified proofs; induction rule is now curried

Replaced Konrad's own add_term_names by the predefined one. Replaced fn Free x => x by dest_Free.

tuned command line;

tuned;

under construction;

SYNC;

fix spelling;

the new README;

now generated automatically from README.html;

README generation;

removed Cambridge font server;

fixed bash path;

reset make_html afterwards;

fixed spelling;