src/HOLCF/IOA/ABP/Correctness.ML
2004-02-19 paulson 2004-02-19 removal of the legacy ML structure List
2003-04-05 nipkow 2003-04-05 Map.empty is now a translation
2001-11-15 wenzelm 2001-11-15 GPLed;
1999-10-27 oheimb 1999-10-27 added various little lemmas
1999-07-08 paulson 1999-07-08 tidied proofs to cope with default if_weak_cong
1998-07-24 berghofe 1998-07-24 Adapted to new datatype package.
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const
1998-03-06 nipkow 1998-03-06 expand_if is now by default part of the simpset.
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-03 nipkow 1997-11-03 expand_list_case -> split_list_case
1997-10-24 nipkow 1997-10-24 Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-07-17 mueller 1997-07-17 changes neede for introducing fairness
1997-06-13 mueller 1997-06-13 changed compatible definition;
1997-04-30 mueller 1997-04-30 Old ABP files now running under the IOA meta theory based on HOLCF;