isabelle update -u control_cartouches;

more symbols;

isabelle update_cartouches -c -t;

modernized header uniformly as section;

eliminated spurious semicolons;

avoid non-standard simp default rule

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'

revert junk submitted by mistake

unbreak "only" option of Sledgehammer

updated some headers;

modernized specifications;

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

More streamlining using metis.

sledgehammer used to streamline protocol proofs

Adapted to new inductive definition package.

new and updated protocol proofs by Giamp Bella

changes due to new neq_simproc in simpdata.ML

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

converting more HOL-Auth to new-style theories

tidying of Isar scripts

tuned parentheses in relational expressions;

Changed 1 to 1' (= Suc 0)

minor tweaks

converted many HOL/Auth theories to Isar scripts

streamlined a proof

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

tidying

partial conversion to Isar script style
simplified unicity proofs

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

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.

set_of_list -> set

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)

Changing from the Reveal to the Oops rule

Addition of Revl rule, and tidying

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

No longer assumes Alice is not the Enemy in NS3.
Proofs do not need it, and the assumption complicated the liveness argument

Reformatting

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