isabelle update_cartouches -c -t;

modernized header uniformly as section;

avoid non-standard simp default rule

renewing specifications in HOL-Auth

updated some headers;

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

Adapted to new inductive definition package.

migrated theory headers to new format

Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes

improved presentation of HOL/Auth theories

Changes required by the certified email protocol

Public-key model now provides separate signature/encryption keys and also
long-term symmetric keys.

tidying of Isar scripts

renaming of evs in the Fake rule

misc tidying; changing the predicate isSymKey to the set symKeys

Streamlining for the bug fix in Blast.
MPair_parts now built in using AddSEs, throughout.

partial conversion to Isar script style
simplified unicity proofs

Got rid of not_Says_to_self and most uses of ~= in definitions and theorems

Global change: lost->bad and sees Spy->spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems

Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition

Deleted the superfluous assumption A ~= B, which must hold anyway by induction

Changing "lost" from a parameter of protocol definitions to a constant.

Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.

set_of_list -> set

Cosmetic improvements

Now with Andy Gordon's treatment of freshness to replace newN/K

New treatment of nonce creation

Extensive tidying and simplification, largely stemming from
changing newN and newK to take an integer argument

Public-key examples