| Thu, 17 May 2007 19:49:16 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:29:39 +0200 |
huffman |
add classes ring_no_zero_divisors and dom
|
file |
diff |
annotate
|
| Thu, 10 May 2007 02:51:53 +0200 |
huffman |
new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
|
file |
diff |
annotate
|
| Mon, 26 Mar 2007 14:53:01 +0200 |
haftmann |
naming tuned
|
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:15 +0100 |
haftmann |
prefix of class interpretation not mandatory any longer
|
file |
diff |
annotate
|
| Wed, 14 Feb 2007 10:06:12 +0100 |
haftmann |
added class "preorder"
|
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, 27 Sep 2006 01:18:35 +0200 |
huffman |
more lemmas about Standard and star_of
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 00:54:10 +0200 |
huffman |
define new constant Standard = range star_of
|
file |
diff |
annotate
|
| Wed, 20 Sep 2006 00:24:24 +0200 |
wenzelm |
renamed axclass_xxxx axclasses;
|
file |
diff |
annotate
|
| Sat, 16 Sep 2006 18:04:14 +0200 |
huffman |
int_diff_cases moved to Integ/IntDef.thy
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 21:36:26 +0200 |
huffman |
add instance for class division_ring
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:46:22 +0200 |
huffman |
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 23:14:41 +0200 |
huffman |
added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:11:46 +0200 |
huffman |
class instances for nonstandard types
|
file |
diff |
annotate
|