| Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:37 +0100 |
haftmann |
moved algebraic classes to Ring_and_Field
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:22 +0200 |
haftmann |
more localisation
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 14:29:59 -0700 |
huffman |
clean up proofs of sign rules for multiplication; add list of lemmas mult_sign_intros
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 19:43:21 +0100 |
nipkow |
merged
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 19:36:04 +0100 |
nipkow |
1. New cancellation simprocs for common factors in inequations
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 03:24:35 -0700 |
huffman |
move field lemmas into class locale context
|
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
|
| Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 15:01:53 -0800 |
huffman |
generalize int_dvd_cancel_factor simproc to idom class
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 06:59:33 -0800 |
huffman |
lemmas abs_dvd_iff, dvd_abs_iff
|
file |
diff |
annotate
|
| Mon, 16 Feb 2009 19:11:55 +0100 |
haftmann |
more default simp rules for sgn
|
file |
diff |
annotate
|
| 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
|
| Tue, 30 Oct 2007 08:45:54 +0100 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Thu, 25 Oct 2007 19:27:50 +0200 |
haftmann |
various localizations
|
file |
diff |
annotate
|
| Thu, 25 Oct 2007 13:52:00 +0200 |
haftmann |
localized further
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 11:48:08 +0200 |
haftmann |
partially localized
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 09:20:58 +0200 |
haftmann |
moved lemmas to OrderedGroup.thy
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 18:17:38 +0200 |
wenzelm |
linorder_neqE_ordered_idom: proper proof, avoid illegal schematic type vars;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 01:21:48 +0200 |
nipkow |
final(?) iteration of sgn saga.
|
file |
diff |
annotate
|
| Thu, 30 Aug 2007 21:43:31 +0200 |
nipkow |
added constant sgn
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:21:33 +0200 |
paulson |
revised blacklisting for ATP linkup
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:14:18 +0200 |
haftmann |
moved class dense_linear_order to Orderings.thy
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:01 +0200 |
haftmann |
split class abs from class minus
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 18:42:09 +0200 |
huffman |
convert instance proofs to Isar style
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:28:36 +0200 |
huffman |
rename class dom to ring_1_no_zero_divisors
|
file |
diff |
annotate
|