src/HOLCF/HOLCF.ML
2005-04-02 huffman 2005-04-02 converted to new-style theory
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-03 wenzelm 2001-11-03 GPLed;
2000-07-04 paulson 2000-07-04 removed most batch-style proofs
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-09-09 mueller 1997-09-09 moved extended adm_tac to new place
1996-12-09 sandnerr 1996-12-09 simpset extension moved from HOLCF.ML to One.ML and Tr2.ML
1996-01-30 clasohm 1996-01-30 expanded tabs
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
1994-06-20 nipkow 1994-06-20 Franz Regensburger's changes.
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.