src/HOL/hologic.ML
Tue, 29 Nov 2005 22:52:19 +0100 wenzelm added mk_split;
Tue, 16 Aug 2005 13:54:24 +0200 nipkow added listT
Mon, 01 Aug 2005 19:20:24 +0200 wenzelm removed read_cterm;
Thu, 14 Jul 2005 19:28:17 +0200 wenzelm removed not_const -- use Not instead;
Mon, 16 May 2005 10:29:15 +0200 paulson Use of IntInf.int instead of int in most numeric simprocs; avoids
Mon, 09 May 2005 16:40:11 +0200 paulson choice_const moved to hologic.ML
Wed, 23 Mar 2005 12:09:18 +0100 paulson replaced bool by a new datatype "bit" for binary numerals
Tue, 08 Mar 2005 16:02:52 +0100 obua fix integer overflow in numeral syntax for SML NJ.
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.
Fri, 20 Aug 2004 12:21:03 +0200 paulson proof reconstruction for external ATPs
Mon, 19 Jul 2004 18:14:57 +0200 berghofe Added function dest_list.
Thu, 01 Jul 2004 12:29:53 +0200 paulson new treatment of binary numerals
Sun, 15 Feb 2004 10:46:37 +0100 paulson Polymorphic treatment of binary arithmetic using axclasses
Fri, 11 Jul 2003 14:56:30 +0200 berghofe mk_int now produces specific constants for 0 and 1.
Tue, 27 May 2003 17:39:17 +0200 berghofe Added pair_const.
Mon, 16 Dec 2002 13:43:11 +0100 berghofe Added mk_int and mk_list.
Mon, 09 Dec 2002 10:38:56 +0100 ballarin Fixed bug in simpdata.ML that prevented the use of congruence rules from a
Thu, 10 Oct 2002 14:23:47 +0200 berghofe Added list_all.
Sat, 01 Dec 2001 18:52:32 +0100 wenzelm renamed class "term" to "type" (actually "HOL.type");
Wed, 17 Oct 2001 18:51:03 +0200 wenzelm added mk_UNIV;
Thu, 04 Oct 2001 15:40:05 +0200 wenzelm added dest_concls;
Thu, 27 Sep 2001 22:23:40 +0200 wenzelm made unit type local;
Mon, 18 Dec 2000 14:59:05 +0100 nipkow moved mk_bin from Numerals to HOLogic
Fri, 03 Nov 2000 21:31:53 +0100 wenzelm removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
Tue, 05 Sep 2000 18:48:22 +0200 wenzelm added not_const;
Sun, 30 Jul 2000 13:02:14 +0200 wenzelm added atomic_Trueprop;
Sun, 16 Jul 2000 20:54:24 +0200 wenzelm added is_unitT;
Sun, 23 Apr 2000 11:39:56 +0200 paulson number_of now takes a type arg
Tue, 18 Apr 2000 15:54:56 +0200 paulson added number_of_const: term
Mon, 13 Mar 2000 13:17:52 +0100 wenzelm added Not;
Sun, 27 Feb 2000 15:22:14 +0100 wenzelm added dest_conj;
Tue, 22 Feb 2000 21:39:01 +0100 wenzelm added boolN;
Wed, 05 Jan 2000 11:56:04 +0100 wenzelm replaced HOLogic.termTVar by HOLogic.termT;
Mon, 04 Oct 1999 14:45:35 +0200 wenzelm added mk_conj, mk_disj, mk_imp;
Tue, 21 Sep 1999 14:13:45 +0200 nipkow ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
Tue, 03 Aug 1999 13:15:20 +0200 paulson added realT
Fri, 23 Jul 1999 17:25:27 +0200 paulson added boolean and binary constants
Wed, 17 Mar 1999 13:46:23 +0100 wenzelm added dest_mem;
Fri, 18 Dec 1998 11:00:15 +0100 paulson new function dest_eq
Tue, 28 Jul 1998 16:59:15 +0200 wenzelm tuned;
Tue, 30 Jun 1998 20:41:41 +0200 berghofe Moved most of the Prod_Syntax - stuff to HOLogic.
Wed, 14 Jan 1998 10:30:44 +0100 wenzelm added unit and prod stuff;
Tue, 23 Dec 1997 11:39:03 +0100 paulson Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
Wed, 26 Nov 1997 16:43:42 +0100 wenzelm added dest_nat;
Mon, 06 Oct 1997 19:15:02 +0200 wenzelm eliminated raise_term, raise_typ;
Thu, 16 Jan 1997 16:53:15 +0100 wenzelm binary oprations and relations;
Fri, 03 Mar 1995 12:02:25 +0100 clasohm new version of HOL with curried function application
less more (0) tip