| Wed, 04 Mar 2009 11:44:05 +0100 |
haftmann |
consequent rewrite of index_size, size [index] to nat_of; support pseudo-primrec sepcifications with fun
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 09:05:19 +0100 |
haftmann |
mandatory prefix for index conversion operations
|
file |
diff |
annotate
|
| Wed, 29 Oct 2008 11:33:40 +0100 |
haftmann |
explicit check for pattern discipline before code translation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 10:17:22 +0200 |
haftmann |
non left-linear equations for nbe
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:24 +0200 |
haftmann |
evaluation using code generator
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 17:54:18 +0200 |
krauss |
more function -> fun
|
file |
diff |
annotate
|
| Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:33 +0200 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:37:05 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2008 19:38:13 +0100 |
haftmann |
yet another useful lemma
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 07:59:57 +0100 |
haftmann |
Zero/Suc recursion combinator for type index
|
file |
diff |
annotate
|
| Sun, 17 Feb 2008 06:49:53 +0100 |
huffman |
New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
|
file |
diff |
annotate
|
| Tue, 29 Jan 2008 10:19:56 +0100 |
haftmann |
treating division by zero properly
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:46 +0100 |
haftmann |
fixed and tuned
|
file |
diff |
annotate
|
| Wed, 23 Jan 2008 09:57:55 +0100 |
haftmann |
yet another OCaml fix
|
file |
diff |
annotate
|
| Tue, 22 Jan 2008 23:06:58 +0100 |
haftmann |
fixed OCaml
|
file |
diff |
annotate
|
| Mon, 21 Jan 2008 08:43:27 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:21 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:23 +0100 |
haftmann |
index now a copy of nat rather than int
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 14:37:00 +0100 |
haftmann |
switched from PreList to ATP_Linkup
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 13:21:12 +0100 |
haftmann |
duv, mod, int conversion
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 10:26:18 +0200 |
haftmann |
added
|
file |
diff |
annotate
|