Wed, 11 Mar 2009 19:27:04 +0100 |
wenzelm |
renamed (unused?) "split.splits" to split_splits -- it was only accepted by accident;
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Mon, 02 Mar 2009 16:53:55 +0100 |
nipkow |
name changes
|
file |
diff |
annotate
|
Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
Fri, 20 Feb 2009 23:46:03 +0100 |
nipkow |
Removed redundant lemmas
|
file |
diff |
annotate
|
Tue, 17 Feb 2009 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
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
|
Mon, 14 Jul 2008 16:13:58 +0200 |
chaieb |
Simplified proofs
|
file |
diff |
annotate
|
Fri, 04 Apr 2008 13:40:27 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Wed, 02 Apr 2008 15:58:36 +0200 |
haftmann |
tuned towards code generation
|
file |
diff |
annotate
|
Mon, 17 Mar 2008 16:13:05 +0100 |
huffman |
remove unneeded constant mod_alt
|
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, 15 Feb 2008 16:09:12 +0100 |
haftmann |
<= and < on nat no longer depend on wellfounded relations
|
file |
diff |
annotate
|
Mon, 21 Jan 2008 08:43:37 +0100 |
haftmann |
tuned proof
|
file |
diff |
annotate
|
Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
Wed, 09 Jan 2008 19:23:50 +0100 |
nipkow |
added simp attributes/ proofs fixed
|
file |
diff |
annotate
|
Mon, 10 Dec 2007 11:24:06 +0100 |
haftmann |
explicit import of theory Main
|
file |
diff |
annotate
|
Thu, 08 Nov 2007 20:08:00 +0100 |
wenzelm |
eliminated illegal schematic variables in where/of;
|
file |
diff |
annotate
|
Tue, 28 Aug 2007 20:13:47 +0200 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
Thu, 23 Aug 2007 18:53:53 +0200 |
huffman |
remove unused lemmas
|
file |
diff |
annotate
|
Wed, 22 Aug 2007 16:44:35 +0200 |
huffman |
move if_simps from BinBoolList to Num_Lemmas
|
file |
diff |
annotate
|
Tue, 21 Aug 2007 20:59:35 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
Tue, 21 Aug 2007 17:24:57 +0200 |
huffman |
move BIT datatype stuff from Num_Lemmas to BinGeneral
|
file |
diff |
annotate
|
Mon, 20 Aug 2007 23:35:51 +0200 |
huffman |
remove redundant lemma int_number_of
|
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
|