| 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
|
| 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
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 16:21:03 +0200 |
nipkow |
hid constant "dom"
|
file |
diff |
annotate
|
| Thu, 24 May 2007 16:52:54 +0200 |
obua |
Squared things out.
|
file |
diff |
annotate
|
| Tue, 22 May 2007 16:47:22 +0200 |
huffman |
add missing instance declarations
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:16 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 17 May 2007 18:32:17 +0200 |
huffman |
added classes ring_no_zero_divisors and dom (non-commutative version of idom);
|
file |
diff |
annotate
|
| Thu, 17 May 2007 08:42:51 +0200 |
huffman |
instance division_ring < no_zero_divisors; clean up field instance proofs
|
file |
diff |
annotate
|
| Sun, 06 May 2007 21:49:29 +0200 |
haftmann |
added auxiliary lemmas for proof tools
|
file |
diff |
annotate
|
| Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:08 +0100 |
haftmann |
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:21 +0100 |
haftmann |
now using "class"
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 15:43:05 +0100 |
haftmann |
dropped Inductive dependency
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 00:43:12 +0100 |
huffman |
added lemma mult_mono'
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 09:33:47 +0100 |
krauss |
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
|
file |
diff |
annotate
|
| Wed, 20 Sep 2006 00:24:24 +0200 |
wenzelm |
renamed axclass_xxxx axclasses;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 18:13:10 +0200 |
obua |
renamed axclass_xxxx axclasses
|
file |
diff |
annotate
|
| Sun, 10 Sep 2006 05:34:24 +0200 |
huffman |
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 16:00:34 +0200 |
obua |
Moved stuff from Ring_and_Field to Matrix
|
file |
diff |
annotate
|
| Wed, 11 Jan 2006 11:00:26 +0100 |
paulson |
tidied, and added missing thm divide_less_eq_1_neg
|
file |
diff |
annotate
|
| Mon, 09 Jan 2006 13:28:06 +0100 |
paulson |
simplified the special-case simprules
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
file |
diff |
annotate
|
| Sat, 25 Jun 2005 16:06:17 +0200 |
nipkow |
Changes due to new abel_cancel.ML
|
file |
diff |
annotate
|
| Wed, 04 May 2005 10:42:43 +0200 |
nipkow |
fixed lin.arith
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 10:59:31 +0200 |
obua |
Removed mult_commute axiom from comm_semiring axclass.
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 18:19:55 +0100 |
obua |
Cleaning up HOL/Matrix
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
| Tue, 05 Oct 2004 15:30:50 +0200 |
paulson |
new simprules for abs and for things like a/b<1
|
file |
diff |
annotate
|
| Mon, 04 Oct 2004 15:28:03 +0200 |
paulson |
revised simprules for division
|
file |
diff |
annotate
|
| Fri, 10 Sep 2004 20:04:14 +0200 |
nipkow |
Added antisymmetry simproc
|
file |
diff |
annotate
|
| Fri, 03 Sep 2004 17:10:36 +0200 |
obua |
Matrix theory, linear programming
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Mon, 26 Jul 2004 17:34:52 +0200 |
paulson |
converting Hyperreal/Transcendental to Isar script
|
file |
diff |
annotate
|
| Tue, 29 Jun 2004 11:18:34 +0200 |
kleing |
license change to BSD
|
file |
diff |
annotate
|
| Mon, 14 Jun 2004 14:20:55 +0200 |
obua |
Further development of matrix theory
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:16:51 +0200 |
wenzelm |
removed duplicate thms;
|
file |
diff |
annotate
|
| Tue, 18 May 2004 10:01:44 +0200 |
obua |
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 20:33:16 +0200 |
nipkow |
Moved ring stuff from ex into Ring_and_Field.
|
file |
diff |
annotate
|
| Thu, 15 Apr 2004 14:17:45 +0200 |
nipkow |
Added ex/Exceptions.thy
|
file |
diff |
annotate
|
| Thu, 01 Apr 2004 10:54:32 +0200 |
paulson |
new type class abelian_group
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:48:22 +0100 |
paulson |
new thms
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
| Mon, 01 Mar 2004 13:51:21 +0100 |
paulson |
new Ring_and_Field hierarchy, eliminating redundant axioms
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Thu, 05 Feb 2004 10:45:28 +0100 |
paulson |
tidying up, especially the Complex numbers
|
file |
diff |
annotate
|
| Thu, 29 Jan 2004 16:51:17 +0100 |
paulson |
simplifications in the hyperreals
|
file |
diff |
annotate
|
| Wed, 28 Jan 2004 10:41:49 +0100 |
paulson |
converted Real/Lubs to Isar script. Converting arithmetic setup
|
file |
diff |
annotate
|
| Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|