src/HOL/Import/Generate-HOL/GenHOL4Base.thy
Thu, 01 Jul 2010 16:54:44 +0200 "prod" and "sum" replace "*" and "+" respectively
Thu, 10 Jun 2010 12:24:03 +0200 tuned quotes, antiquotations and whitespace
Fri, 19 Feb 2010 14:47:01 +0100 moved remaning class operations from Algebras.thy to Groups.thy
Wed, 10 Feb 2010 14:12:04 +0100 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Thu, 28 Jan 2010 11:48:49 +0100 new theory Algebras.thy for generic algebraic structures
Wed, 04 Mar 2009 10:47:20 +0100 Made Option a separate theory and renamed option_map to Option.map
Fri, 12 Oct 2007 08:25:48 +0200 moved class power to theory Power
Fri, 20 Jul 2007 14:28:25 +0200 moved class ord from Orderings.thy to HOL.thy
Tue, 10 Jul 2007 09:23:12 +0200 constant dvd now in class target
Wed, 30 May 2007 21:09:13 +0200 updated
Sat, 19 May 2007 11:33:57 +0200 constant op @ now named append
Thu, 17 May 2007 19:49:40 +0200 canonical prefixing of class constants
Sat, 18 Nov 2006 00:20:24 +0100 dvd_def now with object equality
Fri, 17 Mar 2006 09:34:23 +0100 renamed op < <= to Orderings.less(_eq)
Fri, 10 Mar 2006 15:33:48 +0100 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
Sat, 24 Sep 2005 16:43:41 +0200 HOL4-Import: map ONTO to Fun.surj
Wed, 21 Sep 2005 18:04:49 +0200 new header syntax;
Mon, 29 Aug 2005 16:51:39 +0200 Updated import.
Fri, 17 Jun 2005 16:12:49 +0200 migrated theory headers to new format
Fri, 01 Apr 2005 18:59:17 +0200 Updated import configuration.
Sat, 17 Apr 2004 23:53:35 +0200 Minor cleanup of headers and some speedup of the HOL4 import.
Fri, 02 Apr 2004 17:37:45 +0200 Added HOL proof importer.