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;

adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'

use case_of_simps

simplifier uses proper Proof.context instead of historic type simpset;

Introduction of metis calls and other cosmetic modifications.

modernized primrec

tidied using inductive_simps

updated some headers;

common base for protocols with symmetric keys

--HG--
rename : src/HOL/Auth/ROOT.ML => src/HOL/Auth/All_Symmetric.thy

renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

simplified method setup;

unified type Proof.method and pervasive METHOD combinators;

tuned ML bindings (for multithreading);

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

simplified method setup;

tactic/method simpset: maintain proper context;

replacement of bool by a datatype (making problems first-order). More lemma names

theorems need names

migrated theory headers to new format

local_cla/simpset_of;

avoid \...\;

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

new, separate specifications

Tidying and replacement of some axioms by specifications

improved presentation of HOL/Auth theories

converting more HOL-Auth to new-style theories

tidying

tidying of Isar scripts

Slightly generalized the agents' knowledge theorems

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

misc tidying; changing the predicate isSymKey to the set symKeys

partial conversion to Isar script style
simplified unicity proofs

`` -> ` and ``` -> ``

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

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".

Deleted the obsolete operators newK, newN and nPair

Modified a few defs and proofs because of the changes to theory Finite.thy.

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

Temporary additions (random) for the nested Otway-Rees protocol
They will need to be rationalized

Updating of comments

Weaking of injectivity assumptions for newK and newN:
they are no longer assumed injective over all traces, merely over the
length of a trace

New version of axiom sees1_Says:
Previously it only allowed the SENDER to see the content of messages...
Now instead the RECIPIENT sees the messages. This change had no effect
on subsequent proofs because protocol rules refer specifically to the
relevant messages sent to an agent.

Simple tidying

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

Removal of the Notes constructor

"bad" set simplifies statements of many theorems

Stronger proofs; work for Otway-Rees

Renaming and simplification

Separation of theory Event into two parts:
Shared for general shared-key material
NS_Shared for the Needham-Schroeder shared-key protocol