src/HOL/IMPP/Hoare.thy
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-03-25 wenzelm 2015-03-25 prefer local fixes;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
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-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without 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 rename_tac'd scripts
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2013-05-24 haftmann 2013-05-24 use generic data for code symbols for unified "code_printing" syntax for custom serialisations
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-03-30 wenzelm 2011-03-30 modernized specifications;
2011-01-12 wenzelm 2011-01-12 eliminated global prems;
2010-11-28 nipkow 2010-11-28 gave more standard finite set rules simp and intro attribute
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-03-03 wenzelm 2010-03-03 cleanup type translations;
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-06-25 wenzelm 2008-06-25 modernized specifications;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 proper context for tactics derived from res_inst_tac;
2007-07-21 wenzelm 2007-07-21 tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-06-07 wenzelm 2006-06-07 removed obsolete ML files;
2005-09-17 wenzelm 2005-09-17 converted to Isar theory format;
2001-01-09 nipkow 2001-01-09 *** empty log message ***
2000-01-31 oheimb 2000-01-31 added IMPP to HOL