src/HOLCF/Pcpo.ML
2005-07-26 huffman brought ML files up to date with new lemmas
2005-03-02 huffman converted to new-style theory
2004-06-21 kleing Merged in license change from Isabelle2004
2001-12-12 wenzelm isatool expandshort;
2001-11-03 wenzelm GPLed;
2001-05-31 oheimb added lub_range_mono and lub_range_shift
2000-09-15 paulson renamed (most of...) the select rules
2000-07-05 paulson massive tidy-up: goal -> Goal, remove use of prems, etc.
2000-06-28 paulson tidying and unbatchifying
1998-03-10 oheimb renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
1997-11-03 wenzelm isatool fixclasimp;
1997-10-10 wenzelm fixed dots;
1997-09-29 paulson fast_tac HOL_cs -> Fast_tac, etc.
1997-05-25 slotosch Moved the classes flat chfin from Fix to Pcpo.
1997-05-25 slotosch eliminated the constant less by the introduction of the axclass sq_ord
1997-03-25 slotosch changed some theorems from pcpo to cpo
1997-02-17 slotosch Changes of HOLCF from Oscar Slotosch:
1996-12-18 oheimb removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
1996-12-16 paulson Removed a rogue TAB
1996-12-13 oheimb adaptions for symbol font
1996-12-09 sandnerr added theorems
1996-11-29 oheimb renamed is_flat to flat,
1996-09-26 paulson Ran expandshort; used stac instead of ssubst
1996-05-31 oheimb introduced forgotten bind_thm calls
1996-04-23 oheimb adapted several proofs
1996-01-30 clasohm expanded tabs
1995-10-04 clasohm added local simpsets
1995-04-13 regensbu adjusted HOLCF for new hyp_subst_tac
1995-02-07 clasohm added qed, qed_goal[w]
1994-06-29 clasohm added parentheses made necessary by change of constrain's precedence
1994-01-19 nipkow Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
less more (0) tip