src/HOL/IMP/Denotation.ML
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-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-06-23 paulson 1997-06-23 Ran expandshort
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-10 nipkow 1996-09-10 Converted proofs to use default clasets.
1996-05-08 paulson 1996-05-08 Updated for new form of induction rules
1996-04-27 nipkow 1996-04-27 A completely new version of IMP.
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
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-03-03 clasohm 1995-03-03 new version of HOL/IMP with curried function application