Congruence rules use == in premises now. New class linord.

minor improvements

re-arranged bindings for many function keys

extended input syntax to handle names of special keys

moved Ctrl entry before Alt entry extended input syntax to handle names of special keys

New theorem eq_imp_le

Four new Union/Intersection laws

corrected problem with auto_tac: now uses a variant of depth_tac that avoids interference of the simplifier with dup_step_tac

added New Jersey mirror;

Improved loop-test for rewrite rules a little. Should be done properly!

tuned comment;

added append (curried);

*** empty log message ***

Sign.merge vs. Sign.nontriv_merge;

tuned comments;

oops;

tuned print_cs;

updated;

tuned;

added explicit signature; improved comments;

improved comments;

fixed add_trrules: intern root;

export map_trrule;

tuned add_trrules;

improved is_letter etc.;

New Addsimps for Compl rules

New AddIffs le_0_eq and neq0_conv

Replaced ALLNEWSUBGOALS by THEN_ALL_NEW

Used THEN_ALL_NEW.

moved freeze_thaw to drule.ML

Tidying; rotate_prems; moved freeze_thaw from tactic.ML

AC and other rewrite rules for Un and Int

auto update

Added reference to rotate_prems

filter_size -> length_filter

Added `remdups' nodup -> nodups

added Vartab: TABLE;

added param;

added THEN_ALL_NEW;

New theorem Image_id

New theorem order_eq_refl

New max, min theorems

Added some more explicit guarantees of key secrecy for agents Deleted spurious A~=Spy assumptions

Fixed a lot of overfull and underfull lines (hboxes)

Updated the description of how to set up hyp_subst_tac

New example, Pow_Sigma_bij

fixed WWW links

Three new facts about Image

Replaced \\1 by $1 as Perl itself asked me to...

Fixed the description of recdef

tuned msgs;

improved tracing of rewrite rule application;

removed dead messy code;

added read_var;

tuned;

Updated MOD reference

added symbols syntax;

reorganized into individual theories;

tuned;

make images;