src/HOLCF/Lift.thy
2010-10-27 huffman 2010-10-27 add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
2010-10-27 huffman 2010-10-27 rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
2010-10-22 huffman 2010-10-22 remove finite_po class
2010-10-22 huffman 2010-10-22 simplify proofs about flift; remove unneeded lemmas
2010-10-21 huffman 2010-10-21 minimize imports
2010-10-21 huffman 2010-10-21 pcpodef (open) 'a lift
2010-10-12 huffman 2010-10-12 remove unneeded lemmas Lift_exhaust, Lift_cases
2010-10-12 huffman 2010-10-12 move lemmas from Lift.thy to Cfun.thy
2010-10-12 huffman 2010-10-12 remove unneeded lemmas from Fun_Cpo.thy
2010-10-11 huffman 2010-10-11 new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
2010-10-09 huffman 2010-10-09 move all bifinite class instances to Bifinite.thy
2010-10-08 huffman 2010-10-08 rename class 'sfp' to 'bifinite'
2010-10-06 huffman 2010-10-06 major reorganization/simplification of HOLCF type classes: removed profinite/bifinite classes and approx function; universal domain uses approx_chain locale instead of bifinite class; ideal_completion locale does not use 'take' functions, requires countable basis instead; replaced type 'udom alg_defl' with type 'sfp'; replaced class 'rep' with class 'sfp'; renamed REP('a) to SFP('a);
2010-05-23 huffman 2010-05-23 declare a few more cont2cont rules
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-03-24 huffman 2010-03-24 remove ancient continuity tactic
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-12-11 wenzelm 2008-12-11 pcpodef package: state two goals, instead of encoded conjunction;
2008-06-20 huffman 2008-06-20 remove unused constant liftpair
2008-06-20 huffman 2008-06-20 simplify profinite class axioms
2008-06-20 huffman 2008-06-20 tuned
2008-06-10 haftmann 2008-06-10 rep_datatype command now takes list of constructors as input arguments
2008-05-19 huffman 2008-05-19 instantiation lift :: (countable) bifinite
2008-03-27 huffman 2008-03-27 declare cont_lemmas_ext as simp rules individually
2008-01-16 huffman 2008-01-16 change class axiom ax_flat to rule_format
2008-01-04 huffman 2008-01-04 new instance proofs for classes finite_po, chfin, flat
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');
2006-06-02 wenzelm 2006-06-02 removed obsolete ML files;
2006-05-01 huffman 2006-05-01 add theorem flift2_defined_iff
2006-04-13 huffman 2006-04-13 add lemma less_UU_iff as default simp rule
2005-11-05 huffman 2005-11-05 renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
2005-09-23 wenzelm 2005-09-23 adm_tac/cont_tacRs: proper simpset;
2005-07-08 huffman 2005-07-08 replaced old continuity rules with new lemma cont2cont_lift_case
2005-07-08 huffman 2005-07-08 renamed upE1 to upE; added simp rule cont2cont_flift1
2005-07-07 huffman 2005-07-07 removed obsolete continuity theorems
2005-07-07 huffman 2005-07-07 define lift type using pcpodef; cleaned up
2005-07-05 huffman 2005-07-05 simplified definitions of flift1, flift2, liftpair; added theorem cont2cont_flift1; renamed strictness and definedness theorems
2005-07-01 huffman 2005-07-01 added theorem lift_definedE; moved cont_if to Cont.thy
2005-06-23 huffman 2005-06-23 add binder syntax for flift1
2005-06-14 huffman 2005-06-14 renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
2005-06-03 huffman 2005-06-03 renamed variable in cont2cont_app
2005-05-31 wenzelm 2005-05-31 tuned;
2005-05-25 huffman 2005-05-25 shorted proof that lift is chfin
2005-05-23 huffman 2005-05-23 moved continuity simproc to Cont.thy
2005-05-06 huffman 2005-05-06 Replaced all unnecessary uses of SOME with THE or LEAST
2005-04-02 huffman 2005-04-02 Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
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
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2003-07-11 oheimb 2003-07-11 corrected markup text
2001-12-01 wenzelm 2001-12-01 renamed class "term" to "type" (actually "HOL.type");
2001-11-03 wenzelm 2001-11-03 rep_datatype lift; converted to new-style theory;
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