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