src/HOL/Tools/specification_package.ML
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.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-05-21 wenzelm 2004-05-21 Sign.typ_instance;
2004-04-17 skalberg 2004-04-17 Minor cleanup of headers and some speedup of the HOL4 import.
2003-10-09 skalberg 2003-10-09 Added support for making constants final, that is, ensuring that no definition can be given later (useful for constants whose behaviour is fixed axiomatically rather than definitionally).
2003-10-08 skalberg 2003-10-08 Added axiomatic specifications (ax_specification).
2003-08-27 skalberg 2003-08-27 Improved the error messages (slightly).
2003-08-26 skalberg 2003-08-26 Cleaned up the code.
2003-08-26 skalberg 2003-08-26 Allowed for splitting the specification over several lemmas.
2003-07-21 skalberg 2003-07-21 Added handling of meta implication and meta quantification.
2003-07-21 skalberg 2003-07-21 Added handling of free variables (provided they are of sort HOL.type).
2003-07-21 skalberg 2003-07-21 Changed bstring argument to xstring.
2003-07-21 skalberg 2003-07-21 *** empty log message ***
2003-07-19 skalberg 2003-07-19 Added optional theorem names for the constant definitions added during specification.
2003-07-17 skalberg 2003-07-17 Added package for definition by specification.