src/HOL/Hoare/Hoare.thy
2010-02-23 haftmann 2010-02-23 merged
2010-02-23 haftmann 2010-02-23 dropped axclass; dropped Id; session theory Hoare.thy
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations;
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-22 haftmann 2009-07-22 set intersection and union now named inter and union
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;
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2008-10-02 wenzelm 2008-10-02 major cleanup of hoare_tac.ML: just one copy for Hoare.thy and HoareAbort.thy (only 1 line different), refrain from inspecting the main goal, proper context;
2007-08-29 wenzelm 2007-08-29 added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
2007-08-29 wenzelm 2007-08-29 removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2005-10-07 wenzelm 2005-10-07 print_translation: does not handle _idtdummy;
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-03-11 nipkow 2003-03-11 *** empty log message ***
2002-12-22 nipkow 2002-12-22 removed some problems with print translations
2002-11-29 nipkow 2002-11-29 added a few lemmas
2002-11-06 nipkow 2002-11-06 a new pointer example and some syntactic sugar
2002-10-28 nipkow 2002-10-28 conversion ML -> thy
2001-09-27 wenzelm 2001-09-27 renamed "()" to Unity;
2000-07-21 prensani 2000-07-21 Updating of some comments
1999-01-04 nipkow 1999-01-04 Version 1.0 of linear nat arithmetic.
1998-10-14 nipkow 1998-10-14 New many-sorted version.
1998-09-25 paulson 1998-09-25 patched obsolete code
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-09 wenzelm 1998-06-09 nonterminals prog;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-04-04 nipkow 1997-04-04 renamed variable 'inv'
1997-03-03 wenzelm 1997-03-03 added comment: print translations do not mark tokens;
1996-11-27 paulson 1996-11-27 Replaced obsolete "makestring" by Int.toString
1996-06-25 berghofe 1996-06-25 Changed argument order of nat_rec.
1996-03-08 clasohm 1996-03-08 added constdefs section
1996-02-05 clasohm 1996-02-05 expanded tabs; incorporated Konrad's changes
1995-12-01 clasohm 1995-12-01 removed quotes from types section
1995-11-29 clasohm 1995-11-29 removed quotes from consts and syntax sections
1995-11-17 nipkow 1995-11-17 New directory. Hoare logic according to Mike Gordon.