src/HOL/NanoJava/AxSem.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2015-12-30 wenzelm 2015-12-30 more symbols;
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;
2011-12-13 wenzelm 2011-12-13 modernized specifications;
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-04-23 wenzelm 2011-04-23 modernized specifications;
2011-01-16 wenzelm 2011-01-16 tuned headers;
2010-03-03 wenzelm 2010-03-03 cleanup type translations;
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.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2002-02-25 oheimb 2002-02-25 Clarification wrt. use of polymorphic variants of Hoare logic rules
2001-10-15 oheimb 2001-10-15 renamed reset_locs to del_locs
2001-09-21 oheimb 2001-09-21 Minor improvements, added Example
2001-09-10 oheimb 2001-09-10 marginally improved comments
2001-09-10 oheimb 2001-09-10 corrected antiquotations in comment
2001-09-10 oheimb 2001-09-10 simplified vnam/vname, introduced fname, improved comments
2001-08-30 oheimb 2001-08-30 cosmetics
2001-08-30 oheimb 2001-08-30 removed imname, uncurried Meth
2001-08-09 oheimb 2001-08-09 corrected initialization of locals, streamlined Impl
2001-08-08 oheimb 2001-08-08 layout, subscripts
2001-08-08 oheimb 2001-08-08 changed to full expressions with side effects
2001-07-23 oheimb 2001-07-23 cosmetics
2001-06-16 oheimb 2001-06-16 added NanoJava