src/HOLCF/domain/theorems.ML
2006-01-14 wenzelm 2006-01-14 generic attributes;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-11-30 huffman 2005-11-30 reimplement Case expression pattern matching to support lazy patterns
2005-11-08 huffman 2005-11-08 generate pattern combinators for new datatypes
2005-11-03 huffman 2005-11-03 reimplement copy_def to use data constructor constants
2005-11-03 huffman 2005-11-03 cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
2005-11-02 wenzelm 2005-11-02 dist_eqI: the_context();
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-12 huffman 2005-10-12 domain package generates compactness lemmas for new constructors
2005-10-10 huffman 2005-10-10 replaced foldr' with foldr1
2005-09-17 wenzelm 2005-09-17 removed obsolete BasisLibrary;
2005-07-14 wenzelm 2005-07-14 tuned;
2005-07-12 huffman 2005-07-12 use qualified names for all constants
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-18 huffman 2005-06-18 make match_rews into simp rules by default
2005-06-15 huffman 2005-06-15 Domain package uses ContProc for beta reduction
2005-06-14 huffman 2005-06-14 in domain declarations, selector names are now optional
2005-06-14 huffman 2005-06-14 up_eq and up_less in default simpset now
2005-06-08 huffman 2005-06-08 faster proofs of inverts and injects lemmas, with fewer strictness hypotheses
2005-06-04 huffman 2005-06-04 Domain package generates match functions for new datatypes, for use with the fixrec package
2005-04-16 huffman 2005-04-16 speed improvements for the domain package
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-05-29 wenzelm 2004-05-29 Sign.infer_types: Sign.pp;
2002-08-05 berghofe 2002-08-05 Replaced nat_ind_tac by induct_tac.
2001-11-03 wenzelm 2001-11-03 adapted to new-style theories;
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