isabelle update -u control_cartouches;

more symbols;

prefer abbreviations for compound operators INFIMUM and SUPREMUM

more symbols;

isabelle update_cartouches -c -t;

proper context for assume_tac (atac remains as fall-back without context);

modernized header uniformly as section;

updated some headers;

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

sledgehammer used to streamline protocol proofs

tuned ML bindings (for multithreading);

tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);

Adapted to new inductive definition package.

more robust syntax for definition/abbreviation/notation;

replaced syntax/translations by abbreviation;

migrated theory headers to new format

Conversion of all main protocols from "Shared" to "Public".
Removal of Key_supply_ax: modifications to possibility theorems.
Improved presentation.

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

improved presentation of HOL/Auth theories

tweaks

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

tuned parentheses in relational expressions;

minor tweaks

better treatment of methods: uses Method.ctxt_args to refer to current
simpset and claset. Needed to fix problems with Recur.thy

(rough) conversion of Auth/Recur to Isar format

Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Streamlining of Yahalom proofs
Removal of redundant proofs

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

Tidying

Simplified proofs by omitting PA = {|XA, ...|} from RA2

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

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.

Corrected indentations and margins after the renaming of "set_of_list"

set_of_list -> set

Re-ordering of certificates so that session keys appear in decreasing order

Improved layout and updated comments

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

Simplification of some proofs, especially by eliminating
the equality in RA2

Now uses HPair

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

Recursive Authentication Protocol