src/HOLCF/domain/axioms.ML
2005-07-12 huffman 2005-07-12 use qualified names for all constants
2005-06-14 huffman 2005-06-14 in domain declarations, selector names are now optional
2005-06-09 wenzelm 2005-06-09 add_axioms_infer -- avoids use of stale theory;
2005-06-04 huffman 2005-06-04 Domain package generates match functions for new datatypes, for use with the fixrec package
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
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.
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
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_axioms_i; 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.
1997-11-04 oheimb 1997-11-04 * removed "axioms" and "generated by" section * replaced "ops" section by extended "consts" section, which is capable of handling the continuous function space "->" directly * domain package: now uses normal mixfix annotations (instead of cinfix...)
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-27 oheimb 1997-10-27 adapted domain and ax_ops package for name spaces
1997-10-02 wenzelm 1997-10-02 fully qualified names: Theory.add_XXX;
1997-02-17 slotosch 1997-02-17 using types one = unit lift and translations causes troubles between the type one and the constant one. The later was changed to ONE
1996-12-19 oheimb 1996-12-19 corrected headers
1996-04-03 oheimb 1996-04-03 Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
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