src/HOLCF/Pcpo.thy
2010-10-04 huffman 2010-10-04 new lemmas about lub
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 renamed expand_*_eq in HOLCF as well
2010-03-01 huffman 2010-03-01 add lemma lub_eq
2009-11-08 wenzelm 2009-11-08 modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;
2009-05-08 huffman 2009-05-08 rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
2009-05-08 haftmann 2009-05-08 localized (complete) partial order classes
2009-04-29 huffman 2009-04-29 reimplement reorientation simproc using theory data
2009-01-26 haftmann 2009-01-26 explicit constraints
2009-01-22 haftmann 2009-01-22 simplified handling of base sort, dropped axclass
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-09-17 wenzelm 2008-09-17 back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
2008-07-01 huffman 2008-07-01 remove redundant instance proof finite_po < cpo
2008-07-01 huffman 2008-07-01 replace lub (range Y) with (LUB i. Y i)
2008-03-29 wenzelm 2008-03-29 replaced 'ML_setup' by 'ML';
2008-01-31 huffman 2008-01-31 add lemma cpo_lubI
2008-01-31 huffman 2008-01-31 new discrete_cpo axclass
2008-01-17 huffman 2008-01-17 convert lemma lub_mono to rule_format
2008-01-17 huffman 2008-01-17 rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
2008-01-17 huffman 2008-01-17 change class axiom chfin to rule_format
2008-01-16 huffman 2008-01-16 change class axiom ax_flat to rule_format
2008-01-14 huffman 2008-01-14 class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
2008-01-03 huffman 2008-01-03 new lemma flat_less_iff
2008-01-03 huffman 2008-01-03 new axclass finite_po < finite, po
2008-01-02 huffman 2008-01-02 new class dcpo; added dcpo versions of some lemmas
2007-12-20 huffman 2007-12-20 move bottom-related stuff back into Pcpo.thy
2007-12-18 huffman 2007-12-18 add class ppo of pointed partial orders; define UU in class ppo instead of pcpo; add new lemmas about lub
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2007-04-04 wenzelm 2007-04-04 ML antiquotes;
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-04-13 huffman 2006-04-13 add lemma less_UU_iff as default simp rule
2006-02-04 huffman 2006-02-04 UU_reorient_simproc no longer rewrites UU = numeral
2005-10-10 huffman 2005-10-10 cleaned up
2005-07-07 huffman 2005-07-07 add UU_reorient_simproc
2005-07-01 huffman 2005-07-01 cleaned up
2005-07-01 huffman 2005-07-01 cleaned up
2005-06-03 huffman 2005-06-03 added theorem ch2ch_lub
2005-06-03 huffman 2005-06-03 added theorems diag_lub and ex_lub
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-05-06 huffman 2005-05-06 Replaced all unnecessary uses of SOME with THE or LEAST
2005-03-31 huffman 2005-03-31 chfin now a subclass of po, proved instance chfin < cpo
2005-03-08 huffman 2005-03-08 arranged for document generation, cleaned up some proofs
2005-03-04 huffman 2005-03-04 fix headers
2005-03-04 huffman 2005-03-04 converted to new-style theories, and combined numbered files
2005-03-02 huffman 2005-03-02 converted to new-style theory
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2001-11-09 wenzelm 2001-11-09 eliminated old "symbols" syntax, use "xsymbols" instead;
2001-11-03 wenzelm 2001-11-03 GPLed;
1998-09-09 oheimb 1998-09-09 simplified definition of axclass cpo
1998-03-10 oheimb 1998-03-10 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-25 slotosch 1997-05-25 Moved the classes flat chfin from Fix to Pcpo. Corresponding theorems from Fix into Pcpo,Cont,Cfun3
1997-02-17 slotosch 1997-02-17 Changes of HOLCF from Oscar Slotosch: 1. axclass instead of class * less instead of less_fun, less_cfun, less_sprod, less_cprod, less_ssum, less_up, less_lift * @x.!y.x<<y instead of UUU instead of UU_fun, UU_cfun, ... * no witness type void needed (eliminated Void.thy.Void.ML) * inst_<typ>_<class> derived as theorems 2. improved some proves on less_sprod and less_cprod * eliminated the following theorems Sprod1.ML: less_sprod1a Sprod1.ML: less_sprod1b Sprod1.ML: less_sprod2a Sprod1.ML: less_sprod2b Sprod1.ML: less_sprod2c Sprod2.ML: less_sprod3a Sprod2.ML: less_sprod3b Sprod2.ML: less_sprod4b Sprod2.ML: less_sprod4c Sprod3.ML: less_sprod5b Sprod3.ML: less_sprod5c Cprod1.ML: less_cprod1b Cprod1.ML: less_cprod2a Cprod1.ML: less_cprod2b Cprod1.ML: less_cprod2c Cprod2.ML: less_cprod3a Cprod2.ML: less_cprod3b 3. new classes: * cpo<po, * chfin<pcpo, * flat<pcpo, * derived: flat<chfin to do: show instances for lift 4. Data Type One * Used lift for the definition: one = unit lift * Changed the constant one into ONE 5. Data Type Tr * Used lift for the definition: tr = bool lift * adopted definitions of if,andalso,orelse,neg * only one theory Tr.thy,Tr.ML instead of Tr1.thy,Tr1.ML, Tr2.thy,Tr2.ML * reintroduced ceils for =TT,=FF 6. typedef * Using typedef instead of faking type definitions to do: change fapp, fabs from Cfun1 to Rep_Cfun, Abs_Cfun 7. adopted examples and domain construct to theses changes These changes eliminated all rules and arities from HOLCF
1996-12-13 oheimb 1996-12-13 adaptions for symbol font
1996-12-02 oheimb 1996-12-02 removed 8bit sections
1996-11-29 oheimb 1996-11-29 *** empty log message ***
1996-02-06 clasohm 1996-02-06 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
1994-10-10 nipkow 1994-10-10 corrected problems with changed binding power of ::.
1994-10-06 nipkow 1994-10-06 New version