src/HOLCF/domain/theorems.ML
2001-11-03 wenzelm 2001-11-03 GPLed;
2001-08-31 berghofe 2001-08-31 Renamed functions % and %% to avoid clash with syntax for proof terms.
2001-01-09 nipkow 2001-01-09 ` -> $
2000-10-17 paulson 2000-10-17 tidying and renaming of contrapos rules
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
2000-01-28 oheimb 2000-01-28 added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
1999-10-21 wenzelm 1999-10-21 get_thm;
1999-01-12 wenzelm 1999-01-12 eliminated tthm type and Attribute structure;
1998-08-12 slotosch 1998-08-12 eliminated fabs,fapp. changed all theorem names and functions into Rep_CFun, Abs_CFun
1998-04-29 wenzelm 1998-04-29 adapted to new PureThy.add_tthmss; Theory.parent_path;
1998-03-24 oheimb 1998-03-24 added cproj', and therefore extended prj tried to fix polymorphism problem for take_defs. A full solution will require significant changes.
1998-03-10 oheimb 1998-03-10 renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
1997-11-21 wenzelm 1997-11-21 changed Pure/Sequence interface -- isatool fixseq;
1997-11-20 wenzelm 1997-11-20 tuned infer_types interface;
1997-11-12 wenzelm 1997-11-12 structure BasisLibrary;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New way of referring to Basis Library
1997-10-30 oheimb 1997-10-30 domain package: * theorems are stored in the theory * creates hierachical name space * minor changes to some names and values (for consistency), e.g. cases -> casedist, dists_eq -> dist_eqs, [take_lemma] -> take_lemmas * separator between mutual domain definitions changed from "," to "and" * minor debugging of Domain_Library.mk_var_names
1997-10-29 oheimb 1997-10-29 debugging concerning sort variables theorems are now proved immediately after generating the syntax
1997-10-27 oheimb 1997-10-27 adapted domain and ax_ops package for name spaces
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-04-24 nipkow 1997-04-24 Updates because nat_ind_tac no longer appends "1" to the ind.var.
1996-12-18 oheimb 1996-12-18 The previous log message was wrong. The correct one is: generalized handling of type expressions, type variables and sorts
1996-12-18 oheimb 1996-12-18 removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
1996-11-29 oheimb 1996-11-29 modified file headers renamed lift to fup
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map Tried to tidy up the indenting...
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-06-27 oheimb 1996-06-27 re-added when_funs to library.ML
1996-06-26 oheimb 1996-06-26 function names in when_rews now meta-quantified
1996-05-31 oheimb 1996-05-31 adapted use of monofun_cfun_arg
1996-04-23 oheimb 1996-04-23 *** empty log message ***
1996-04-04 oheimb 1996-04-04 Removed 8bit characters used by mistake
1996-04-03 oheimb 1996-04-03 *** empty log message ***
1996-04-03 oheimb 1996-04-03 Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-30 clasohm 1996-01-30 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