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

*** empty log message ***

reflecting my recent changes of the classical reasoner

reflecting my recent changes of the simplifier and classical reasoner

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),

cosmetic

updated mini_ss

added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss, safe_asm_more_full_simp_tac new addss (old version retained as unsafe_addss), new auto_tac (old version retained as unsafe_auto_tac), clasimpset with modification functions

corrected minor mistakes

description of safe vs. unsafe wrapper and the functions involved

moved THEN_MAYBE to Pure/tctical.ML better addbefore, addafter (now: addaltern), setwrapper (now: setWrapper) and addwrapper (now addWrapper) added safe wrapper(and functions setSWrapper,compSWrapper,addSbefore,addSaltern)

added deleqcongs, richer rep_ss split solver in safe and unsafe parts (finish_tac, unsafe_finish_tac) added safe_asm_full_simp_tac, setSSolver, addSSolver renamed setsolver to setSolver, addsolver to addSolver

description of del(eq)congs, safe and unsafe solver

added THEN_MAYBE and THEN_MAYBE'

added del_congs

Some lemmas changed to valuesd

fixed comment;

improved interface options;

semi fix of piping-quit peoblem (should work on systems with *real* sh);

globally unset ENV, BASH_ENV;

Made troublesome simplifier warning dependent on trace_simp.

Modified and shortened adm_disj lemmas.

Deleted a useless definition

Added optimization: do nothing for empty list