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