src/HOL/IMPP/Hoare.thy
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