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
|
Tue, 03 Jul 2007 01:26:06 +0200 |
huffman |
instance pordered_comm_ring < pordered_ring
|
file |
diff |
annotate
|
Sat, 30 Jun 2007 17:30:10 +0200 |
obua |
added ordered_ring and ordered_semiring
|
file |
diff |
annotate
|
Mon, 25 Jun 2007 15:19:18 +0200 |
nipkow |
removed redundant lemmas
|
file |
diff |
annotate
|
Sun, 24 Jun 2007 21:15:55 +0200 |
nipkow |
tex problem fixed
|
file |
diff |
annotate
|
Sun, 24 Jun 2007 20:55:41 +0200 |
nipkow |
tuned and used field_simps
|
file |
diff |
annotate
|
Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
Sun, 17 Jun 2007 18:47:03 +0200 |
nipkow |
tuned laws for cancellation in divisions for fields.
|
file |
diff |
annotate
|
Sun, 17 Jun 2007 13:39:29 +0200 |
chaieb |
added theorems nonzero_mult_divide_cancel_right' nonzero_mult_divide_cancel_left' ordered_field_no_lb ordered_field_no_ub
|
file |
diff |
annotate
|
Sat, 16 Jun 2007 15:01:54 +0200 |
nipkow |
The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
|
file |
diff |
annotate
|
Fri, 15 Jun 2007 15:10:32 +0200 |
nipkow |
made divide_self a simp rule
|
file |
diff |
annotate
|