Tidying of signature. More robust renaming in freeze_thaw. New tactic distinct_subgoals_tac

Removal of freeze_vars and thaw_vars (quite unused...)

Removal of radixstring from string_of_int; addition of string_of_indexname

There was never need for another copy of radixstring...

Numerous simplifications and removal of HOL-isms Addition of the "simpset" feature (replacing references to \!simpset)

Now loads theory Recdef

A slight simplification of optstring The new "simpset" keyword in the "recdef" declaration

Now extracts the predicate variable from induct0 insteead of trying to predict its name. The new "freeze" function requires this.

Deleted the obsolete "pred_list" relation

Documented the new distinct_subgoals_tac

A slight simplification of optstring

Now extracts the predicate variable from induct0 insteead of trying to predict its name

Made the pseudo-type of split_rule_var a separate argument

eliminated non-ASCII;

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