src/HOLCF/Lift3.ML
1998-08-12 slotosch 1998-08-12 eliminated fabs,fapp. changed all theorem names and functions into Rep_CFun, Abs_CFun
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Renamed expand_const -> split_const
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-06-23 paulson 1997-06-23 Ran expandshort
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-20 mueller 1997-05-20 deleted duplicate rewrite rules of lift.simps
1997-04-24 mueller 1997-04-24 expandshort
1997-04-24 mueller 1997-04-24 Complete Redesign of Theory, main points are: - Extension of the continuity prover: * Lemmas about continuity of flift1 and flift2 are generalized * Lemmas about continuity of mixed definitions of HOL and LCF terms generalized Pay attention: Sometimes proofs are shorter now! - a number of new lemmas concerning flift1, flift2, Def and Undef, Def_less_is_eq (Def x << y = (Def x = y)) and lemmas characterizing flift1 and flift2 are added to !simpset Pay attention: Sometimes proofs are shorter now! - added tactic def_tac for eliminating x~=UU in assumptions
1997-03-26 nipkow 1997-03-26 Added "discrete" CPOs and modified IMP to use those rather than "lift"
1997-02-17 slotosch 1997-02-17 reflecting recent changes of the simplifier
1997-02-17 oheimb 1997-02-17 reflecting recent changes of the simplifier
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 changed handling of cont_lemmas and adm_lemmas
1996-12-09 sandnerr 1996-12-09 Headers added
1996-12-09 sandnerr 1996-12-09 Theories Lift1, Lift2 and Lift3 inserted below HOLCF.thy
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-04-23 oheimb 1996-04-23 adapted several proofs
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-10 regensbu 1995-10-10 corrected some errors that occurred after introduction of local simpsets
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-10-04 clasohm 1995-10-04 added local simpsets
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
1995-02-07 clasohm 1995-02-07 added qed, qed_goal[w]
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.