src/HOL/Auth/Message.thy
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-28 wenzelm 2015-12-28 more symbols;
2015-12-10 wenzelm 2015-12-10 isabelle update_cartouches -c -t;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-19 wenzelm 2015-03-19 more position information;
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-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-06-27 paulson 2014-06-27 tiny refinements
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-12 wenzelm 2013-04-12 removed historic comments;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-08-12 huffman 2011-08-12 make more HOL theories work with separate set type
2011-06-28 paulson 2011-06-28 keyfree: The set of key-free messages (and associated theorems)
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-26 wenzelm 2011-04-26 simplified/modernized method setup;
2011-02-18 wenzelm 2011-02-18 modernized specifications;
2011-02-02 paulson 2011-02-02 Introduction of metis calls and other cosmetic modifications.
2010-09-08 paulson 2010-09-08 tidied using inductive_simps
2010-07-22 wenzelm 2010-07-22 updated some headers;
2010-03-04 paulson 2010-03-04 Simplified a couple of proofs and corrected a comment
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
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