src/HOL/Tools/specification_package.ML
Thu, 21 Apr 2005 18:57:18 +0200 berghofe Adapted to new interface of instantiation and unification / matching functions.
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Fri, 21 May 2004 21:15:45 +0200 wenzelm Sign.typ_instance;
Sat, 17 Apr 2004 23:53:35 +0200 skalberg Minor cleanup of headers and some speedup of the HOL4 import.
Thu, 09 Oct 2003 18:13:32 +0200 skalberg Added support for making constants final, that is, ensuring that no
Wed, 08 Oct 2003 16:02:54 +0200 skalberg Added axiomatic specifications (ax_specification).
Wed, 27 Aug 2003 10:11:30 +0200 skalberg Improved the error messages (slightly).
Tue, 26 Aug 2003 19:33:35 +0200 skalberg Cleaned up the code.
Tue, 26 Aug 2003 18:49:17 +0200 skalberg Allowed for splitting the specification over several lemmas.
Mon, 21 Jul 2003 17:27:23 +0200 skalberg Added handling of meta implication and meta quantification.
Mon, 21 Jul 2003 16:19:34 +0200 skalberg Added handling of free variables (provided they are of sort HOL.type).
Mon, 21 Jul 2003 08:53:56 +0200 skalberg Changed bstring argument to xstring.
Mon, 21 Jul 2003 08:52:06 +0200 skalberg *** empty log message ***
Sat, 19 Jul 2003 17:35:15 +0200 skalberg Added optional theorem names for the constant definitions added during
Thu, 17 Jul 2003 15:23:20 +0200 skalberg Added package for definition by specification.
less more (0) tip