src/HOLCF/Cfun1.thy
1998-08-12 slotosch 1998-08-12 eliminated fabs,fapp. changed all theorem names and functions into Rep_CFun, Abs_CFun
1997-11-04 oheimb 1997-11-04 simplified (and corrected) syntax definition of fapp
1997-06-04 mueller 1997-06-04 changed priority of -> from [6,5]5 to [1,0]0
1997-05-25 slotosch 1997-05-25 eliminated the constant less by the introduction of the axclass sq_ord added explicit type ::'a::po in the following theorems: minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair and dist_eqI (in domain-package) added instances instance fun :: (term,sq_ord)sq_ord instance "->" :: (term,sq_ord)sq_ord instance "**" :: (sq_ord,sq_ord)sq_ord instance "*" :: (sq_ord,sq_ord)sq_ord instance "++" :: (pcpo,pcpo)sq_ord instance u :: (sq_ord)sq_ord instance lift :: (term)sq_ord instance discr :: (term)sq_ord
1997-03-25 slotosch 1997-03-25 changed continuous functions from pcpo to cpo (including instances)
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
1996-12-13 oheimb 1996-12-13 adaptions for symbol font
1996-12-02 oheimb 1996-12-02 in Tools/8bit/isa-patches/HOLCF/clean-HOLCF.cfg
1996-11-29 oheimb 1996-11-29 *** empty log message ***
1996-11-29 oheimb 1996-11-29 renamed is_flat to flat, moved Lift*.* to Up*.*, renaming of all constans and theorems concerned, (*lift* to *up*, except Ilift to Ifup, lift to fup)
1996-02-06 clasohm 1996-02-06 expanded tabs
1995-10-06 regensbu 1995-10-06 added 8bit pragmas added directory ax_ops for sections axioms and ops added directory domain for sections domain and generated this is the type definition package of David Oheimb
1995-06-29 regensbu 1995-06-29 The curried version of HOLCF is now just called HOLCF. The old uncurried version is no longer supported
1994-06-20 nipkow 1994-06-20 Franz Regensburger's changes.
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.