isabelle update -u control_cartouches;

more symbols;

standardized towards new-style formal comments: isabelle update_comments;

"split add" -> "split"

more symbols;

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;

updated news

use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries

enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions

--HG--
extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893

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

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

modernized specifications;

removed spurious addition from 9e58f0499f57;

Tidied up proofs using sledgehammer, also deleting unnecessary semicolons

modernized primrec

updated some headers;

tuned header

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.);

tuned Proof

stripped some legacy bindings

simplified method setup;

more robust syntax for definition/abbreviation/notation;

replaced syntax/translations by abbreviation;

tactic/method simpset: maintain proper context;

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

a few more named lemmas

tidied away duplicate thm

migrated theory headers to new format

deleted a pointless comment

local_cla/simpset_of;

fixed a comment

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

Simplified a proof using presburger

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.

conversion of Auth/TLS to Isar script

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

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

Removal of the obsolete newN function

New treatment of nonce creation

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

Public-key examples