isabelle update -u control_cartouches;

more symbols;

standardized towards new-style formal comments: isabelle update_comments;

isabelle update_cartouches -c -t;

"subgoal" examples

more symbols;

isabelle update_cartouches -c -t;

prefer local fixes;

modernized header uniformly as section;

eliminated obsolete "standard";

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

updated some headers;

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

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

removed atp_minimize invocation

Removal of redundant settings of unification trace and search bounds.

Adapted to new inductive definition package.

a few more named lemmas

changes due to new neq_simproc in simpdata.ML

fixed document;

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

converting more HOL-Auth to new-style theories

tidying of Isar scripts

tuned parentheses in relational expressions;

converted many HOL/Auth theories to Isar scripts

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

updating both Yahalom protocols to the Gets model

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

Tidying

Expressed most Oops rules using Notes instead of Says, and other tidying

Many minor speedups:
1. Some use of rewriting with expand_ifs instead of addsplits[expand_if]
2. Faster proof of new_keys_not_used
3. New version of shrK_neq (no longer refers to "range")

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.

Deleted a redundant A~=B in rules that refer to a previous event

set_of_list -> set

Defines KeyWithNonce, which is used to prove the secrecy of NB

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

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

Removed needless quotation marks

Swapped arguments of Crypt (for clarity and because it is conventional)

Minor changes to comments

New Oops message, with Server as source to ensure
correct nonces

Addition of Reveal message

Introduction of "lost" argument
Changed Enemy -> Spy
Ran expandshort

Addition of Yahalom protocol

Tidied many proofs, using AddIffs to let equivalences take
the place of separate Intr and Elim rules. Also deleted most named clasets.