src/HOLCF/Tr.thy
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
2008-12-16 huffman 2008-12-16 remove cvs Id tags
2008-06-20 huffman 2008-06-20 added some lemmas; reorganized into sections; tuned proofs
2008-06-11 wenzelm 2008-06-11 removed dead code;
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'axiomatization');
2007-10-21 wenzelm 2007-10-21 modernized specifications ('definition', 'abbreviation', 'notation');
2005-11-03 huffman 2005-11-03 changed order of arguments for constant behind If-then-else-fi syntax; added LAM patterns for TT, FF
2005-11-03 huffman 2005-11-03 cleaned up; removed adm_tricks in favor of compactness theorems
2005-07-08 huffman 2005-07-08 simplified proof of ifte_thms, removed ifte_simp
2005-07-01 huffman 2005-07-01 defaultsort pcpo
2005-06-04 huffman 2005-06-04 import Fix is unnecessary
2005-05-31 wenzelm 2005-05-31 tuned;
2005-05-25 wenzelm 2005-05-25 removed LICENCE note -- everything is subject to Isabelle licence as stated in COPYRIGHT file;
2005-04-01 huffman 2005-04-01 convert 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;
2001-01-09 nipkow 2001-01-09 *** empty log message ***
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-05-25 slotosch 1997-05-25 Eliminated ccc1. Moved ID,oo into Cfun.
1997-04-24 mueller 1997-04-24 deleted definitions for blift and plift
1997-03-11 wenzelm 1997-03-11 tr is (again) type abbrev;
1997-03-07 wenzelm 1997-03-07 "bool lift" now syntax instead of type abbrev;
1997-03-04 paulson 1997-03-04 Renamed constant "not" to "Not"
1997-02-17 oheimb 1997-02-17 corrected type of plift
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