| Mon, 26 Apr 2010 11:34:19 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:43 +0100 |
haftmann |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:43:45 +0100 |
berghofe |
Adapted to changes in induct method.
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Tue, 16 Jun 2009 00:01:32 -0700 |
huffman |
smult_dvd lemmas; polynomial gcd
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 14:20:26 +0200 |
haftmann |
farewell to class recpower
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:21 +0200 |
haftmann |
power operation defined generic
|
file |
diff |
annotate
|
| Thu, 16 Apr 2009 10:11:34 +0200 |
haftmann |
tightended specification of class semiring_div
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 10:05:11 +0100 |
haftmann |
normalized imports
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 17:12:23 -0800 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
| Fri, 27 Feb 2009 15:37:56 -0800 |
huffman |
make list-style polynomial syntax work when show_sorts is on
|
file |
diff |
annotate
|
| Mon, 23 Feb 2009 07:19:53 -0800 |
huffman |
add lemmas poly_{div,mod}_minus_{left,right}
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 20:14:45 -0800 |
huffman |
move Polynomial.thy to Library
|
file |
diff |
annotate
| base
|