src/HOL/IMP/Hoare.ML
1997-04-02 paulson 1997-04-02 Replaced Best_tac by the one rule needed for the proof
1997-03-18 nipkow 1997-03-18 Added wp_while.
1996-10-07 paulson 1996-10-07 Ran expandshort
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-10 nipkow 1996-09-10 Converted proofs to use default clasets.
1996-08-19 paulson 1996-08-19 Tidied some proofs, maybe using less_SucE
1996-05-17 nipkow 1996-05-17 Had to rename params because variable names in an induction rule changed.
1996-05-07 paulson 1996-05-07 Updated for new form of induction rules
1996-04-27 nipkow 1996-04-27 A completely new version of IMP.
1996-02-09 nipkow 1996-02-09 Introduced qed_spec_mp.
1996-02-07 nipkow 1996-02-07 Modified datatype com. Added (part of) relative completeness proof for Hoare logic.
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-23 nipkow 1996-01-23 Added a verified verification-condition generator.
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-05-09 nipkow 1995-05-09 Moved induct2 from Hoare to Lfp.
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-07 nipkow 1995-03-07 *** empty log message ***
1995-03-07 nipkow 1995-03-07 Hoare logic