eliminated freeze_vars;

changed priority of -> from [6,5]5 to [1,0]0

is_blank: fixed space2;

No longer refers to internal TFL structures

More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const Changed the TFL functor to a structure (currently called Prim)

New theory "Power" of exponentiation (and binomial coefficients)

New theorem about the cardinality of the powerset (uses exponentiation)

Type inference makes a Const here, perhaps elsewhere?thry.sml

poly_tvars allows recdefs to be made without type constraints

Corrected banner: it is W0, not MiniML

New statement and proof of free_tv_subst_var in order to cope with new rewrite rules Un_insert_left, Un_insert_right

Now Un_insert_left, Un_insert_right are default rewrite rules

Corrected statement of filter_append; added filter_size

Simplified proof

New theorems le_add_diff_inverse, le_add_diff_inverse2

trivial changes to incorporate CTL.thy and Example.ML in html file;

Simplified the calling sequence of CONTEXT_REWRITE_RULE Eliminated get_rhs, which was calling dest_Trueprop too many times

Moved "less_eq" to NatDef from Arith

New results including the basis for unique factorization

Now "primes" is a set

Now Divides must be the parent

New proofs about cardinality. Suggested by Florian Kammueller

Addition of Finite as parent allows cardinality theorems

Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs

Overloading of "^" requires a type constraint

Overloading of "^" requires new type class "power", with types "nat" and "set" in that class. The operator itself is declared in Nat.thy

New theory Divides

Many new theorems about cardinality

Now Divides must be the parent

Moving div and mod from Arith to Divides Moving dvd from ex/Primes to Divides

flushOut ensures that no recent error message are lost (not certain this is necessary)

polyml-3.1 default again (for local work);

fixed -P (checkout only);

NJ 1.09.2x as factory default!

Last changes for new release 94-8

added 1.09.28 note;

New theorems suggested by Florian Kammueller

Restoration of the two "bypassed" theorems Union_quotient and quotient_disj

Removal of card_insert_disjoint, which is now a default rewrite rule

New theorem disjoint_eq_subset_Compl

New theorem le_Suc_eq

Removal of mask.sig and mask.sml

Removal of module Mask and datatype binding with its constructor |->

New theorems suggested by Florian Kammueller

remoded ccc1

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