src/HOL/Isar_examples/HoareEx.thy
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-08-30 webertj 2006-08-30 lin_arith_prover: splitting reverted because of performance loss
2006-07-31 webertj 2006-07-31 lin_arith_prover splits certain operators (e.g. min, max, abs)
2005-11-16 wenzelm 2005-11-16 tuned document;
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2005-05-02 nipkow 2005-05-02 fixed
2005-03-03 nipkow 2005-03-03 fixed proof
2004-07-15 nipkow 2004-07-15 more summation syntax
2002-08-07 nipkow 2002-08-07 Added time example at the end.
2001-10-06 wenzelm 2001-10-06 * sane numerals (stage 2): plain "num" syntax (removed "#");
2001-10-05 wenzelm 2001-10-05 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
2001-01-10 wenzelm 2001-01-10 use \<acute>;
2000-10-03 wenzelm 2000-10-03 Hoare logic in Isar;