src/HOL/IMP/Hoare.ML
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-31 paulson 1998-07-31 Removal of obsolete "open" commands from heads of .ML files
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-03 nipkow 1998-07-03 Removed leading !! in goals.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-05-06 nipkow 1998-05-06 Changed [/] to [:=] and removed actual definition.
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-11-20 paulson 1997-11-20 Got rid of some slow deepen_tac calls
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-29 paulson 1997-09-29 Step_tac -> Safe_tac
1997-04-23 paulson 1997-04-23 Ran expandshort
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