another little bug ;-) and minor changes in TLS.*;

little bug ;-)

added keyword 'and'

corrected Header

Addsimps [max_le_iff_conj]; Addsimps [le_min_iff_conj];

changed Super_L and Hyper_R to left and right Meta

layout

solved conflict by taking newest version;

added Clarify_tac to speed up proofs

moved a theorem

fixed comment

fixed some indenting; changed a VERY slow blast_tac to fast_tac

updated, tuned;

added Minho (Portugal);

Fixed bug (improper handling of flag flat_names).

Added quiet_mode flag.

- Changed structure of name spaces - Proofs for datatypes with unneeded parameters are working now - added additional parameter flat_names - added quiet_mode flag

tuned MLWorks options; added print_depth;

MLWorks 2.0;

Changed structure of name spaces for datatypes.

2. The simplifier now knows a little bit about nat-arithmetic.

Mods because trans_tac is now part of thge simplifier.

Mods because of: Installed trans_tac in solver of simpset().

Installed trans_tac in solver of simpset().

changed tags from 0, 1 to None, Some() to avoid special treatment of 0

parent is Main

*** empty log message ***

integer simprocs

Uses overload_1st_set to specify overloading

specifications as sets of programs

Description of new version.

New many-sorted version.

See (* FIXME zero_neq_conv *)

Nat: added zero_neq_conv List: added nth/update lemmas.

added Int.int;

PRIVATE sig parts;

length_Suc_conv is no longer given to AddIffs

new theorems

tidied

Addition of HOL/UNITY/Client

new rule

Addition of HOL/UNITY/Client

Unified treatment of type error msgs.

More pretty breaks in error msgs.

Added a few breaks in error text.

new theorem

new theorems

new guarantees laws

renamed Suc_card_Diff or something

Multisets at last!

added Induct/Multiset*

New inductive definition of `card'

polymorphic versions of nat_neq_iff and nat_neqE

Further improvement of the simplifier.

Tuned simplifier not to re-normalized already normalized terms.

tuned rm CVS;