src/HOLCF/Ssum0.ML
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const
1998-01-08 oheimb 1998-01-08 added select_equality to the implicit claset
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1996-04-23 oheimb 1996-04-23 adapted several proofs
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-10 regensbu 1995-10-10 corrected some errors that occurred after introduction of local simpsets
1995-10-06 regensbu 1995-10-06 added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-06-29 regensbu 1995-06-29 The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported
1995-02-07 clasohm 1995-02-07 added qed, qed_goal[w]
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.