| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Mon, 26 Jan 2009 22:14:18 +0100 |
haftmann |
stripped Id
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:00:50 -0800 |
huffman |
fixed proofs due to changes in Int.thy
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:42 +0200 |
berghofe |
Deleted subset_antisym in a few proofs, because it is
|
file |
diff |
annotate
|
| Fri, 04 Apr 2008 13:40:24 +0200 |
haftmann |
more new primrec
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:36 +0200 |
haftmann |
tuned towards code generation
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 07:15:40 +0100 |
kleing |
fixed broken bintrunc lemma
|
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, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 20:08:00 +0100 |
wenzelm |
eliminated illegal schematic variables in where/of;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
| Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 00:37:12 +0200 |
huffman |
remove unused lemmas
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 23:37:51 +0200 |
huffman |
remove lemma bin_rec_PM
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 18:52:44 +0200 |
huffman |
import BinInduct;
|
file |
diff |
annotate
|
| Thu, 23 Aug 2007 15:47:42 +0200 |
huffman |
move bin_nth stuff to its own subsection
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 17:24:57 +0200 |
huffman |
move BIT datatype stuff from Num_Lemmas to BinGeneral
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 17:20:41 +0200 |
huffman |
simplify termination proof
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 22:48:24 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 21:31:10 +0200 |
huffman |
reorganize into subsections
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:11:09 +0200 |
huffman |
headers for document generation
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 04:34:31 +0200 |
kleing |
* HOL-Word:
|
file |
diff |
annotate
|