src/HOL/IMP/VC.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;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
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-23 nipkow 1996-08-23 Swaped two conditions in the completeness statement.
1996-05-10 paulson 1996-05-10 Updated for new form of induction rules
1996-02-09 nipkow 1996-02-09 Introduced qed_spec_mp.
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-23 nipkow 1996-01-23 Added vcwp
1996-01-23 nipkow 1996-01-23 Added a verified verification-condition generator.