Mon, 17 Feb 1997 12:00:00 +0100 tuned comments;
wenzelm [Mon, 17 Feb 1997 12:00:00 +0100] rev 2643
tuned comments;
Mon, 17 Feb 1997 11:04:00 +0100 Examples are adopted to the changes from HOLCF.
slotosch [Mon, 17 Feb 1997 11:04:00 +0100] rev 2642
Examples are adopted to the changes from HOLCF. Classlib is reduced. Classlib still uses arities, Classlib will change completely to new classes of ADTs
Mon, 17 Feb 1997 11:01:10 +0100 using types one = unit lift and translations causes troubles between
slotosch [Mon, 17 Feb 1997 11:01:10 +0100] rev 2641
using types one = unit lift and translations causes troubles between the type one and the constant one. The later was changed to ONE
Mon, 17 Feb 1997 10:57:11 +0100 Changes of HOLCF from Oscar Slotosch:
slotosch [Mon, 17 Feb 1997 10:57:11 +0100] rev 2640
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
Sat, 15 Feb 1997 18:24:05 +0100 *** empty log message ***
oheimb [Sat, 15 Feb 1997 18:24:05 +0100] rev 2639
*** empty log message ***
Sat, 15 Feb 1997 17:55:11 +0100 reflecting my recent changes of the classical reasoner
oheimb [Sat, 15 Feb 1997 17:55:11 +0100] rev 2638
reflecting my recent changes of the classical reasoner
Sat, 15 Feb 1997 17:52:31 +0100 reflecting my recent changes of the simplifier and classical reasoner
oheimb [Sat, 15 Feb 1997 17:52:31 +0100] rev 2637
reflecting my recent changes of the simplifier and classical reasoner
Sat, 15 Feb 1997 17:48:19 +0100 added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss,
oheimb [Sat, 15 Feb 1997 17:48:19 +0100] rev 2636
added delcongs, Delcongs, unsafe_solver, safe_solver, HOL_basic_ss, safe_asm_more_full_simp_ta, clasimpset HOL_css with modification functions new addss (old version retained as unsafe_addss), new Addss (old version retained as Unsafe_Addss), new auto_tac (old version retained as unsafe_auto_tac),
Sat, 15 Feb 1997 17:45:08 +0100 cosmetic
oheimb [Sat, 15 Feb 1997 17:45:08 +0100] rev 2635
cosmetic
Sat, 15 Feb 1997 17:44:10 +0100 updated mini_ss
oheimb [Sat, 15 Feb 1997 17:44:10 +0100] rev 2634
updated mini_ss
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip