| Tue, 03 Jul 2007 22:27:11 +0200 |
wenzelm |
assume basic HOL context for compilation (antiquotations);
|
file |
diff |
annotate
|
| Sat, 09 Jun 2007 00:28:46 +0200 |
wenzelm |
simplified type integer;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 22:46:56 +0200 |
wenzelm |
simplified/renamed add_numerals;
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:17 +0200 |
haftmann |
abstract size function in hologic.ML
|
file |
diff |
annotate
|
| 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
|