removed ccc1

tuned comment;

Two useful facts about Powersets suggested by Florian Kammueller

Added a missing "result();" after problem 43.

Tidying using the new exhaust_tac

Now recdef checks the name of the function being defined. Slight tidying

Deleted option_case_tac because exhaust_tac performs a similar function. Deleted the duplicate proof of expand_option_case...

Renamed lessD to Suc_leI

New operator "lists" for formalizing sets of lists

New theorem subset_inj_onto

Two results suggested by Florian Kammueller

Tidying and a couple of useful lemmas

Added recdef

Primrec: New example ported from ZF

Renamed lessD to Suc_leI

New example ported from ZF

Simplified proofs using expand_option_case

Now checks the name of the function being defined; More de-HOL-ification

More de-HOL-ification

Now checks the name of the function being defined

Deleted unused functions

Now a Perl script. No longer requires commands to be at the beginnings of lines. RESTRICTION: no longer expands tabs to spaces. No longer lists the files it is altering.

Slight simplifications

Eliminated ccc1. Moved ID,oo into Cfun.

Moved the classes flat chfin from Fix to Pcpo. Corresponding theorems from Fix into Pcpo,Cont,Cfun3

*** empty log message ***

Eliminated the prediates flat,chfin Changed theorems with flat(x::'a) to (x::'a::flat) Since flat<chfin theorems adm_flat,adm_flatdom are eliminated. Use adm_chain_finite and adm_chfindom instead! Examples do not use flat_flat any more

eliminated the constant less by the introduction of the axclass sq_ord added explicit type ::'a::po in the following theorems: minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair and dist_eqI (in domain-package) added instances instance fun :: (term,sq_ord)sq_ord instance "->" :: (term,sq_ord)sq_ord instance "**" :: (sq_ord,sq_ord)sq_ord instance "*" :: (sq_ord,sq_ord)sq_ord instance "++" :: (pcpo,pcpo)sq_ord instance u :: (sq_ord)sq_ord instance lift :: (term)sq_ord instance discr :: (term)sq_ord

tuned;

arbitrary

Added `arbitrary'

fixed;

new syntactic priority of lambda abstraction

adapted entry for addss, addSss

news.

Documented `size' function for datatypes.

fixed a bug

removed TFL from test;

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;

IMPORTANT NOTE: This is the old README.

X11 font server sample configuration;

deleted duplicate rewrite rules of lift.simps

minor changes

tuned;

added eindhoven http address

Declares Option_ as synonym for structure Option

Removal of redundant code (unused or already present in Isabelle. This eliminates HOL compatibility but makes the code smaller and more readable

Basis library version of type "option" now resides in its own structure Option

Removal of ex/LexProd

Renamed egcd and gcd; defined the gcd function using TFL

Removal of duplicate code from TFL

New arithmetic laws let us delete three lines of a proof

Added comment: it is SLOW

Some theorems moved to HOL/Arith.ML

Relation "less_than" internalizes "<" for easy use of TFL

New pattern-matching definition of pred_nat

The diff laws must be named: we do "Delsimps [diff_Suc];"

New theorems from Hoare/Arith2.ML

new treatment of Prover files

Removal of ex/LexProd; TFL files; new treatment of Prover files

Removal of ex/LexProd