1998-12-02 wenzelm 1998-12-02 tuned;
1998-12-02 wenzelm 1998-12-02 IOA-Storage: Memory storage case study.
1998-01-13 mueller 1998-01-13 added simulations files to IOA;
1998-01-12 mueller 1998-01-12 added further IOA liles;
1998-01-07 wenzelm 1998-01-07 improved targets; fixed dependencies on parent logics;
1997-12-19 wenzelm 1997-12-19 log files; 'clean' target;
1997-11-04 wenzelm 1997-11-04 HOLCFLogic.ML, contconsts.ML renamed to holcf_logic.ML, cont_consts.ML;
1997-11-04 oheimb 1997-11-04 * removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)
1997-10-30 wenzelm 1997-10-30 added adm.ML;
1997-10-20 wenzelm 1997-10-20 removed Dlist;
1997-10-17 wenzelm 1997-10-17 removed Classlib;
1997-07-07 wenzelm 1997-07-07 eliminated chmod -w;
1997-05-26 slotosch 1997-05-26 removed ccc1
1997-05-25 slotosch 1997-05-25 Eliminated the prediates flat,chfin Changed theorems with flat(x::'a) to (x::'a::flat) Since flat<chfin theorems adm_flat,adm_flatdom are eliminated. Use adm_chain_finite and adm_chfindom instead! Examples do not use flat_flat any more
1997-05-15 wenzelm 1997-05-15 remove Witness.thy;
1997-05-06 wenzelm 1997-05-06 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
1997-04-30 mueller 1997-04-30 added IOA (meta theory and ABP, NTP examples);
1997-04-25 wenzelm 1997-04-25 removed -c option;
1997-04-24 wenzelm 1997-04-24 removed space;
1997-04-24 oheimb 1997-04-24 added dependencies on ax_ops/*.ML and domain/*.ML
1997-03-26 nipkow 1997-03-26 Added "discrete" CPOs and modified IMP to use those rather than "lift"
1997-03-20 wenzelm 1997-03-20 isatool usedir;
1997-03-17 nipkow 1997-03-17 Added the HOLCF-based den. sem. of IMP.
1997-02-24 oheimb 1997-02-24 removed explicit_domains/, which is now covered by ex/
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
1997-01-31 oheimb 1997-01-31 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains
1997-01-08 wenzelm 1997-01-08 IsaMakefile for HOLCF;