src/HOL/Auth/Message.thy
2010-02-11 wenzelm 2010-02-11 modernized syntax/translations;
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations;
2009-12-24 paulson 2009-12-24 tidied proofs
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
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-07-21 haftmann 2009-07-21 Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
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;
2008-10-27 paulson 2008-10-27 metis proof
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-16 wenzelm 2008-06-16 eliminated OldGoals.inst;
2008-06-11 wenzelm 2008-06-11 OldGoals.inst;
2008-06-11 wenzelm 2008-06-11 RuleInsts.res_inst_tac with proper context;
2008-06-10 haftmann 2008-06-10 slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
2008-05-07 berghofe 2008-05-07 Replaced blast by fast in proof of parts_singleton, since blast looped because of the new encoding of sets.
2008-03-19 wenzelm 2008-03-19 more antiquotations;
2007-08-01 wenzelm 2007-08-01 tuned ML bindings (for multithreading);
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-05-06 haftmann 2007-05-06 dropped legacy ML binding
2007-03-09 haftmann 2007-03-09 *** empty log message ***
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-09-20 paulson 2006-09-20 tidied
2005-12-22 paulson 2005-12-22 shorter proof
2005-09-30 paulson 2005-09-30 theorems need names
2005-09-28 paulson 2005-09-28 streamlined theory; conformance to recent publication
2005-07-13 paulson 2005-07-13 tidied
2005-07-13 paulson 2005-07-13 generlization of some "nat" theorems
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
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-08-12 paulson 2003-08-12 ZhouGollmann: new example (fair non-repudiation protocol)
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-25 paulson 2003-04-25 Changes required by the certified email protocol Public-key model now provides separate signature/encryption keys and also long-term symmetric keys.
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-04-24 paulson 2001-04-24 (rough) conversion of Auth/Recur to Isar format
2001-04-12 paulson 2001-04-12 converted many HOL/Auth theories to Isar scripts
2001-04-09 paulson 2001-04-09 new theorem Fake_parts_insert_in_Un
2001-03-29 paulson 2001-03-29 misc tidying; changing the predicate isSymKey to the set symKeys
2001-03-05 paulson 2001-03-05 a few basic X-symbols
2001-03-02 paulson 2001-03-02 conversion of Message.thy to Isar format
2001-01-09 nipkow 2001-01-09 `` -> ` and ``` -> ``
2000-08-24 paulson 2000-08-24 xsymbols for {| and |}
1999-07-21 paulson 1999-07-21 tweaked proofs to handle new freeness reasoning for data c onstructors
1999-06-10 paulson 1999-06-10 new translation to allow images over Nonce
1998-10-16 paulson 1998-10-16 parent is Main
1998-08-03 paulson 1998-08-03 Better comments
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-30 berghofe 1998-06-30 Adapted to new inductive definition package.
1997-09-11 paulson 1997-09-11 Split base cases from "msg" to "atomic" in order to reduce the number of freeness theorems
1997-01-17 paulson 1997-01-17 Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-07 paulson 1997-01-07 Incorporation of HPair into Message
1996-12-13 paulson 1996-12-13 Addition of the Hash constructor Strengthening spy_analz_tac
1996-11-29 paulson 1996-11-29 Swapped arguments of Crypt (for clarity and because it is conventional)
1996-10-24 paulson 1996-10-24 Removal of unused predicate isSpy
1996-09-26 paulson 1996-09-26 Introduction of "lost" argument Changed Enemy -> Spy Ran expandshort
1996-09-23 paulson 1996-09-23 Simplification of definition of synth