src/HOL/NanoJava/Equivalence.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
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-09 blanchet 2014-09-09 rename_tac'd scrips
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2010-06-28 haftmann 2010-06-28 explicit is better than implicit
2010-03-01 haftmann 2010-03-01 merged
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-24 wenzelm 2010-02-24 modernized syntax declarations, and make them actually work with authentic syntax;
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-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2003-08-29 ballarin 2003-08-29 Methods rule_tac etc support static (Isar) contexts.
2002-02-25 oheimb 2002-02-25 Clarification wrt. use of polymorphic variants of Hoare logic rules
2002-01-14 oheimb 2002-01-14 cosmetics
2001-12-17 nipkow 2001-12-17 mods due to mor powerful simprocs for 1-point rules (quantifier1).
2001-09-21 oheimb 2001-09-21 Minor improvements, added Example
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-06-16 oheimb 2001-06-16 added NanoJava