src/HOL/Auth/Shared.thy
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2013-09-06 noschinl 2013-09-06 use case_of_simps
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-02-02 paulson 2011-02-02 Introduction of metis calls and other cosmetic modifications.
2010-09-08 haftmann 2010-09-08 merged
2010-09-08 haftmann 2010-09-08 modernized primrec
2010-09-08 paulson 2010-09-08 tidied using inductive_simps
2010-07-22 wenzelm 2010-07-22 updated some headers;
2009-09-21 haftmann 2009-09-21 common base for protocols with symmetric keys
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2007-08-01 wenzelm 2007-08-01 tuned ML bindings (for multithreading);
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-07-08 wenzelm 2006-07-08 tactic/method simpset: maintain proper context;
2006-01-23 paulson 2006-01-23 replacement of bool by a datatype (making problems first-order). More lemma names
2005-10-04 paulson 2005-10-04 theorems need names
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
2004-06-21 wenzelm 2004-06-21 avoid \...\;
2003-09-23 paulson 2003-09-23 Removal of the Key_supply axiom (affects many possbility proofs) and minor changes
2003-09-04 paulson 2003-09-04 new, separate specifications
2003-07-24 paulson 2003-07-24 Tidying and replacement of some axioms by specifications
2003-05-05 paulson 2003-05-05 improved presentation of HOL/Auth theories
2003-04-26 paulson 2003-04-26 converting more HOL-Auth to new-style theories
2003-04-09 paulson 2003-04-09 tidying
2002-08-17 paulson 2002-08-17 tidying of Isar scripts
2001-12-07 paulson 2001-12-07 Slightly generalized the agents' knowledge theorems
2001-04-27 paulson 2001-04-27 better treatment of methods: uses Method.ctxt_args to refer to current simpset and claset. Needed to fix problems with Recur.thy
2001-03-29 paulson 2001-03-29 misc tidying; changing the predicate isSymKey to the set symKeys
2001-02-13 paulson 2001-02-13 partial conversion to Isar script style simplified unicity proofs
2001-01-09 nipkow 2001-01-09 `` -> ` and ``` -> ``
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1997-09-18 paulson 1997-09-18 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
1997-07-14 paulson 1997-07-14 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.
1997-07-11 paulson 1997-07-11 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".
1997-07-01 paulson 1997-07-01 Deleted the obsolete operators newK, newN and nPair
1997-06-05 nipkow 1997-06-05 Modified a few defs and proofs because of the changes to theory Finite.thy.
1997-01-17 paulson 1997-01-17 Now with Andy Gordon's treatment of freshness to replace newN/K
1996-12-19 paulson 1996-12-19 Extensive tidying and simplification, largely stemming from changing newN and newK to take an integer argument
1996-12-13 paulson 1996-12-13 Temporary additions (random) for the nested Otway-Rees protocol They will need to be rationalized
1996-12-05 paulson 1996-12-05 Updating of comments
1996-11-28 paulson 1996-11-28 Weaking of injectivity assumptions for newK and newN: they are no longer assumed injective over all traces, merely over the length of a trace
1996-10-09 paulson 1996-10-09 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.
1996-10-07 paulson 1996-10-07 Simple tidying
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-23 paulson 1996-09-23 Removal of the Notes constructor
1996-09-09 paulson 1996-09-09 "bad" set simplifies statements of many theorems
1996-09-09 paulson 1996-09-09 Stronger proofs; work for Otway-Rees
1996-09-03 paulson 1996-09-03 Renaming and simplification
1996-08-21 paulson 1996-08-21 Separation of theory Event into two parts: Shared for general shared-key material NS_Shared for the Needham-Schroeder shared-key protocol