src/HOL/Isar_examples/Hoare.thy
2007-04-20 haftmann 2007-04-20 reverted to classical syntax for K_record
2007-04-20 haftmann 2007-04-20 tuned syntax: K_record is now an authentic constant
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 schirmer 2006-11-07 field-update in records is generalised to take a function on the field rather than the new value.
2006-09-11 wenzelm 2006-09-11 induct method: renamed 'fixing' to 'arbitrary';
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-02-22 wenzelm 2006-02-22 tuned proofs;
2005-11-23 wenzelm 2005-11-23 tuned induction proofs;
2005-11-16 wenzelm 2005-11-16 tuned document;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2003-03-14 kleing 2003-03-14 fix for changes in HOL/Hoare/
2002-11-09 kleing 2002-11-09 Hoare.ML -> hoare.ML
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-10-30 wenzelm 2001-10-30 tuned induct proofs;
2001-01-12 wenzelm 2001-01-12 tuned;
2001-01-11 wenzelm 2001-01-11 subst syntax;
2001-01-10 wenzelm 2001-01-10 use \<acute>;
2000-12-11 wenzelm 2000-12-11 moved "_update_name" to HOL/Record;
2000-11-06 wenzelm 2000-11-06 improved: 'induct' handle non-atomic goals;
2000-10-03 wenzelm 2000-10-03 Hoare logic in Isar;