| Fri, 02 Mar 2007 15:43:22 +0100 |
haftmann |
added add_numerals_of
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 16:33:11 +0100 |
wenzelm |
simplified mk/dest_numeral (cf. mk/dest_binum of 1.65);
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:45:31 +0100 |
haftmann |
introduced mk/dest_numeral/number for mk/dest_binum etc.
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 11:57:30 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 00:25:02 +0100 |
wenzelm |
binary numerals: restricted to actual abstract syntax;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 19:37:26 +0100 |
wenzelm |
misc cleanup -- removed non-HOL operations;
|
file |
diff |
annotate
|
| Fri, 01 Dec 2006 17:22:31 +0100 |
haftmann |
slight cleanup in hologic.ML
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 13:42:46 +0100 |
haftmann |
added Trueprop_conv
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 00:51:47 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Wed, 22 Nov 2006 10:20:15 +0100 |
haftmann |
incorporated structure HOList into HOLogic
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 14:29:58 +0100 |
wenzelm |
removed obsolete dest_eq_typ;
|
file |
diff |
annotate
|
| Sat, 04 Nov 2006 19:25:40 +0100 |
wenzelm |
removed is_Trueprop (use can dest_Trueprop'' instead);
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 17:07:26 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:21 +0200 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 14:51:24 +0200 |
haftmann |
cleaned up HOL bootstrap
|
file |
diff |
annotate
|
| Mon, 02 Oct 2006 17:33:13 +0200 |
paulson |
added is_Trueprop
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 13:34:16 +0200 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 12:11:56 +0200 |
paulson |
renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
|
file |
diff |
annotate
|
| Tue, 29 Nov 2005 22:52:19 +0100 |
wenzelm |
added mk_split;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:54:24 +0200 |
nipkow |
added listT
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 19:20:24 +0200 |
wenzelm |
removed read_cterm;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:17 +0200 |
wenzelm |
removed not_const -- use Not instead;
|
file |
diff |
annotate
|
| Mon, 16 May 2005 10:29:15 +0200 |
paulson |
Use of IntInf.int instead of int in most numeric simprocs; avoids
|
file |
diff |
annotate
|
| Mon, 09 May 2005 16:40:11 +0200 |
paulson |
choice_const moved to hologic.ML
|
file |
diff |
annotate
|
| Wed, 23 Mar 2005 12:09:18 +0100 |
paulson |
replaced bool by a new datatype "bit" for binary numerals
|
file |
diff |
annotate
|
| Tue, 08 Mar 2005 16:02:52 +0100 |
obua |
fix integer overflow in numeral syntax for SML NJ.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Fri, 20 Aug 2004 12:21:03 +0200 |
paulson |
proof reconstruction for external ATPs
|
file |
diff |
annotate
|
| Mon, 19 Jul 2004 18:14:57 +0200 |
berghofe |
Added function dest_list.
|
file |
diff |
annotate
|
| Thu, 01 Jul 2004 12:29:53 +0200 |
paulson |
new treatment of binary numerals
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 14:56:30 +0200 |
berghofe |
mk_int now produces specific constants for 0 and 1.
|
file |
diff |
annotate
|
| Tue, 27 May 2003 17:39:17 +0200 |
berghofe |
Added pair_const.
|
file |
diff |
annotate
|
| Mon, 16 Dec 2002 13:43:11 +0100 |
berghofe |
Added mk_int and mk_list.
|
file |
diff |
annotate
|
| Mon, 09 Dec 2002 10:38:56 +0100 |
ballarin |
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
|
file |
diff |
annotate
|
| Thu, 10 Oct 2002 14:23:47 +0200 |
berghofe |
Added list_all.
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Wed, 17 Oct 2001 18:51:03 +0200 |
wenzelm |
added mk_UNIV;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2001 15:40:05 +0200 |
wenzelm |
added dest_concls;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:23:40 +0200 |
wenzelm |
made unit type local;
|
file |
diff |
annotate
|
| Mon, 18 Dec 2000 14:59:05 +0100 |
nipkow |
moved mk_bin from Numerals to HOLogic
|
file |
diff |
annotate
|
| Fri, 03 Nov 2000 21:31:53 +0100 |
wenzelm |
removed atomic_Trueprop (now in Pure/Isar/auto_bind.ML);
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:48:22 +0200 |
wenzelm |
added not_const;
|
file |
diff |
annotate
|
| Sun, 30 Jul 2000 13:02:14 +0200 |
wenzelm |
added atomic_Trueprop;
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:54:24 +0200 |
wenzelm |
added is_unitT;
|
file |
diff |
annotate
|
| Sun, 23 Apr 2000 11:39:56 +0200 |
paulson |
number_of now takes a type arg
|
file |
diff |
annotate
|
| Tue, 18 Apr 2000 15:54:56 +0200 |
paulson |
added number_of_const: term
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 13:17:52 +0100 |
wenzelm |
added Not;
|
file |
diff |
annotate
|
| Sun, 27 Feb 2000 15:22:14 +0100 |
wenzelm |
added dest_conj;
|
file |
diff |
annotate
|
| Tue, 22 Feb 2000 21:39:01 +0100 |
wenzelm |
added boolN;
|
file |
diff |
annotate
|
| Wed, 05 Jan 2000 11:56:04 +0100 |
wenzelm |
replaced HOLogic.termTVar by HOLogic.termT;
|
file |
diff |
annotate
|
| Mon, 04 Oct 1999 14:45:35 +0200 |
wenzelm |
added mk_conj, mk_disj, mk_imp;
|
file |
diff |
annotate
|
| Tue, 21 Sep 1999 14:13:45 +0200 |
nipkow |
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
|
file |
diff |
annotate
|
| Tue, 03 Aug 1999 13:15:20 +0200 |
paulson |
added realT
|
file |
diff |
annotate
|
| Fri, 23 Jul 1999 17:25:27 +0200 |
paulson |
added boolean and binary constants
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 13:46:23 +0100 |
wenzelm |
added dest_mem;
|
file |
diff |
annotate
|
| Fri, 18 Dec 1998 11:00:15 +0100 |
paulson |
new function dest_eq
|
file |
diff |
annotate
|
| Tue, 28 Jul 1998 16:59:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|