1999-05-12 wenzelm 1999-05-12 strip_quotes replaced by unenclose;
1998-03-09 wenzelm 1998-03-09 Symbol.explode;
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-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-08-06 wenzelm 1997-08-06 use ThySyn.add_syntax;
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-28 paulson 1996-11-28 Replaced map...~~ by Tried to tidy up the indenting...
1996-11-27 paulson 1996-11-27 Replaced obsolete "makestring" by Bool.toString
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-17 regensbu 1995-10-17 *** empty log message ***
1995-10-17 regensbu 1995-10-17 removed incompatibility with sml
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