isabelle update -u control_cartouches;

more symbols;

standardized towards new-style formal comments: isabelle update_comments;

"split add" -> "split"

isabelle update_cartouches -c -t;

prefer tactics with explicit context;

proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;

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

modernized header uniformly as section;

updated news

renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'

use case_of_simps

prefer high-level elim_format;

eliminated obsolete "standard";

Introduction of metis calls and other cosmetic modifications.

renewing specifications in HOL-Auth

updated some headers;

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

sledgehammer used to streamline protocol proofs

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

eliminated OldGoals.inst;

OldGoals.inst;

tuned ML bindings (for multithreading);

simplified method setup;

more robust syntax for definition/abbreviation/notation;

replaced syntax/translations by abbreviation;

a few more named lemmas

tidied away duplicate thm

migrated theory headers to new format

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

Tidying and replacement of some axioms by specifications

improved presentation of HOL/Auth theories

tweaks

converting more HOL-Auth to new-style theories

Changes required by the certified email protocol

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

three new theorems

spelling check

a few basic X-symbols

conversion of Message.thy to Isar format

partial conversion to Isar script style
simplified unicity proofs

exchanged the order of Gets and Notes in datatype event

Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
Changing "spies" to "knows Spy", etc. Retaining the constant "spies" as a
translation.

Adapted to new datatype package.

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

Spy can see Notes of the compromised agents

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.

Moving common declarations and proofs from theories "Shared"
and "Public" to "Event". NB the original "Event" theory was later renamed "Shared".

Addition of the Notes constructor to datatype "event".

Have been obsolete for months; contents are now in Shared and NS_Shared

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

Renaming and simplification

Addition of message NS5

Working version of NS, messages 1-4!

Working version of NS, messages 1-3, WITH INTERLEAVING

Renaming of functions, and tidying

Works up to main theorem, then XXX...X

Auth proofs work up to the XXX...

Added Msg 3; works up to Says_Server_imp_Key_newK

Proving safety properties of authentication protocols