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

Minor corrections