| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 10:00:31 -0800 |
huffman |
rename plength to psize
|
file |
diff |
annotate
|
| Wed, 14 Jan 2009 13:47:14 -0800 |
huffman |
one more [code del] declaration
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 13:48:21 -0800 |
huffman |
code generation for polynomials
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 13:02:16 -0800 |
huffman |
more [code del] declarations
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 08:19:14 -0800 |
huffman |
declare smult rules [simp]
|
file |
diff |
annotate
|
| Tue, 13 Jan 2009 06:57:08 -0800 |
huffman |
convert Deriv.thy to use new Polynomial library (incomplete)
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 22:41:08 -0800 |
huffman |
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
|
file |
diff |
annotate
|
| Thu, 01 Jan 2009 20:28:03 +0100 |
wenzelm |
avoid implicit prems -- tuned proofs;
|
file |
diff |
annotate
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
| base
|