added Infixl/rName: specify infix name independently from syntax; added Pure symbolfont syntax;

added symbol_font.ML;

added add_modesyntax(_i); improved syntax of ==, =?=, ==> (now allows "op ..."); added Pure symbolfont syntax;

added is_printable: string -> bool;

added Syntax/symbol_font.ML;

Removal of an obsolete result, and authentication of B to A

Changed subst_bounds to subst_bound, to run faster

Optimizations: removal of polymorphic equality; one-argument case for subst_bounds

Speedups involving norm

Introduction of structure Int

Updated and clearer(?) instructions

Modified formal of thms in html file.

removed 'open Syntax Type';

removed silly message;

subsig tuning;

tuned subsig;

Updated version and date

Removal of polymorphic equality via mem, subset, eq_set, etc

In-lined the one function call to normTsh

Removal of polymorphic equality via mem, subset, eq_set, etc

Now moves all Tool/*gif files.

Changed some mem calls to be monomorphic

Changed some mem, ins and union calls to be monomorphic

Changed some mem and ins calls to be monomorphic

Updated syntax; shortened comments; put in monomorphic versions of ins

Removed a call to polymorphic mem

Added a comment

Should never have been added in the first place

A bit of tidying up

Ran expandshort

Removed "standard" call from uresult, to allow specialist applications

Deleted a redundant pattern

Adjusting to new version of uresult

Tidying up: removing redundant assumptions, etc.

Deleted bogus comment

Adding lessI to default claset

tuned fix_shyps a little bit more;

New version of paper.

Replaced the very slow "find" command by "rm" with wildcards

Simplified new_keys_not_seen, etc.: replaced the union over all agents by the Spy alone. Proofs run faster and they do not have to be set up in terms of a previous lemma.

Used nat_trans_tac. New Eta. various smaller changes.

Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes

Removal of now unused sum, max, min. Use foldl op+, Int.max, Int.min

Minor changes to comments

New version with simpler disambiguation in YM3, Oops message, and no encryption in YM2

New, purely illustrative result Crypt_synth_analz

Proof of antisym_less_lift now simpler and more robust

Now uses Int.max instead of max

Changes tabs found in .thy files to spaces

Replaced "sum" (only usage?) by foldl op+

Now uses Int.max instead of max

maxidx_of_typs replaces max o map maxidx_of_typ

Now uses Int.max instead of max nodup_Vars now updates maxidx

maxidx_of_typs replaces max o map maxidx_of_typ Now uses Int.max instead of max

asm_rewrite_goal_tac now calls SELECT_GOAL. Replaced min by Int.min

Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML

Replaced min by Int.min

Deleted Olist constructor. Replaced minidx by "above" function

Now defines structure Int

Changed some mem calls to mem_int for greater efficiency (not that it could matter)

Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%

Changed some mem calls to mem_string for greater efficiency (not that it could matter)

Minor updates

Updated references