| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:26 +0200 |
haftmann |
dropped superfluous code lemmas
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:50:42 +0100 |
wenzelm |
more antiquotations;
|
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
|
| Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:34 +0100 |
haftmann |
dropped legacy ml bindings
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 19:40:24 +0200 |
wenzelm |
tuned LinArith setup;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 19:58:53 +0200 |
nipkow |
Added cancel simprocs for dvd on nat and int
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 03:31:11 +0200 |
huffman |
removed constant int :: nat => int;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 05:20:05 +0200 |
huffman |
modify proofs to avoid referring to int::nat=>int
|
file |
diff |
annotate
|
| Fri, 08 Jun 2007 03:24:27 +0200 |
huffman |
generalize zpower_number_of_{even,odd} lemmas
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 17:01:33 +0200 |
huffman |
generalize class constraints on some lemmas
|
file |
diff |
annotate
|
| Thu, 31 May 2007 18:16:52 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|