more symbols;

isabelle update_cartouches -c -t;

modernized header uniformly as section;

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'

Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

updated some headers;

modernized specifications;

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

Simplified some proofs using metis.

Eliminated most of the neq0_conv occurrences. As a result, many
theorems had to be rephrased with ~= 0 instead of > 0.

fixed proofs

Adapted to new inductive definition package.

more robust syntax for definition/abbreviation/notation;

replaced syntax/translations by abbreviation;

new and updated protocol proofs by Giamp Bella

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

Tidying and replacement of some axioms by specifications

converting more HOL-Auth to new-style theories

tidying of Isar scripts

* sane numerals (stage 2): plain "num" syntax (removed "#");

sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;

Changed 1 to 1' (= Suc 0)

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

New example Kerberos_BAN by G Bella