| 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
|