Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
Mon, 03 Apr 2017 23:12:16 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
Sun, 02 Nov 2014 16:54:06 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
Sun, 21 Sep 2014 16:56:11 +0200 |
haftmann |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
file |
diff |
annotate
|
Tue, 17 Apr 2012 16:21:47 +1000 |
Thomas Sewell |
New tactic "word_bitwise" expands word equalities/inequalities into logic.
|
file |
diff |
annotate
|
Tue, 10 Jan 2012 15:43:16 +0100 |
huffman |
add simp rules for set_bit and msb applied to 0 and 1
|
file |
diff |
annotate
|
Tue, 10 Jan 2012 14:48:42 +0100 |
huffman |
add simp rule test_bit_1
|
file |
diff |
annotate
|
Fri, 30 Dec 2011 16:08:35 +0100 |
huffman |
add simp rules for bitwise word operations with 1
|
file |
diff |
annotate
|
Wed, 28 Dec 2011 13:20:46 +0100 |
huffman |
add several new tests, most of which don't work yet
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 00:08:09 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Sat, 23 Apr 2011 13:00:19 +0200 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
Tue, 27 Jan 2009 13:41:45 +0100 |
wenzelm |
recovered example types from WordMain.thy;
|
file |
diff |
annotate
|
Mon, 26 Jan 2009 22:14:17 +0100 |
haftmann |
tuned header
|
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, 02 Nov 2007 12:35:27 +0100 |
kleing |
Added reference to Jeremy Dawson's paper on the word library.
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 03:49:18 +0200 |
huffman |
Word Examples directory
|
file |
diff |
annotate
|