| Sun, 15 Feb 2009 22:58:02 +0100 |
nipkow |
dvd and setprod lemmas
|
file |
diff |
annotate
|
| Sat, 14 Feb 2009 19:01:31 -0800 |
huffman |
generalize lemma fps_square_eq_iff, move to Ring_and_Field
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 14:12:00 -0800 |
huffman |
add class cancel_comm_monoid_add
|
file |
diff |
annotate
|
| Sun, 08 Feb 2009 11:59:26 +0100 |
nipkow |
added noatps
|
file |
diff |
annotate
|
| Sat, 31 Jan 2009 09:04:16 +0100 |
nipkow |
added some simp rules
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:02:12 +0100 |
haftmann |
added lemma abs_sng
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 23:36:30 -0800 |
huffman |
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
|
file |
diff |
annotate
|
| Mon, 12 Jan 2009 12:10:41 -0800 |
huffman |
declare dvd_minus_iff and minus_dvd_iff [iff]
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 10:43:09 -0800 |
huffman |
add lemma dvd_diff to class comm_ring_1
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 10:26:50 -0800 |
huffman |
add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 10:07:39 -0800 |
huffman |
move lemmas mult_minus{left,right} inside class ring
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 09:58:36 -0800 |
huffman |
clean up division_ring proofs
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:48 +0200 |
haftmann |
tuned default rules of (dvd)
|
file |
diff |
annotate
|
| Fri, 05 Sep 2008 00:19:50 +0200 |
huffman |
instances comm_semiring_0_cancel < comm_semiring_0, comm_ring < comm_semiring_0_cancel
|
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
|
| Thu, 10 Jul 2008 07:15:19 +0200 |
huffman |
by intro_locales -> ..
|
file |
diff |
annotate
|
| Sat, 15 Mar 2008 08:11:15 +0100 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Fri, 07 Mar 2008 13:53:03 +0100 |
haftmann |
clarified proposition
|
file |
diff |
annotate
|
| Mon, 03 Mar 2008 15:37:14 +0100 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:20 +0100 |
haftmann |
further localization
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
| Thu, 06 Dec 2007 19:58:21 +0100 |
nipkow |
R&F: added sgn lemma
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:06 +0100 |
haftmann |
using intro_locales instead of unfold_locales if appropriate
|
file |
diff |
annotate
|
| Wed, 21 Nov 2007 13:42:31 +0100 |
haftmann |
dropped diagnostic commands
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 08:47:30 +0100 |
haftmann |
removed subclass edge ordered_ring < lordered_ring
|
file |
diff |
annotate
|
| Fri, 02 Nov 2007 18:52:58 +0100 |
haftmann |
proper reinitialisation after subclass
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 12:14:24 +0100 |
haftmann |
fixed document preparation
|
file |
diff |
annotate
|