src/HOLCF/IMP/Denotational.ML
2001-01-09 nipkow 2001-01-09 ` -> $
1998-10-07 paulson 1998-10-07 tidied
1998-09-21 oheimb 1998-09-21 improved addbefore and addSbefore improved mechanism for unsafe wrappers
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-05-25 slotosch 1997-05-25 *** empty log message ***
1997-05-25 slotosch 1997-05-25 Eliminated the prediates flat,chfin Changed theorems with flat(x::'a) to (x::'a::flat) Since flat<chfin theorems adm_flat,adm_flatdom are eliminated. Use adm_chain_finite and adm_chfindom instead! Examples do not use flat_flat any more
1997-05-16 oheimb 1997-05-16 renamed unsafe_addss to addss
1997-03-27 nipkow 1997-03-27 Optimized proofs.
1997-03-26 nipkow 1997-03-26 Added "discrete" CPOs and modified IMP to use those rather than "lift"
1997-03-17 nipkow 1997-03-17 The HOLCF-based den. sem. of IMP.