| Wed, 30 May 2007 01:53:38 +0200 |
huffman |
renamed some lemmas in Complex.thy
|
file |
diff |
annotate
|
| Mon, 14 May 2007 18:48:24 +0200 |
huffman |
move lemmas to RealPow.thy; tuned proofs
|
file |
diff |
annotate
|
| Thu, 10 May 2007 03:11:03 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Thu, 10 May 2007 03:07:26 +0200 |
huffman |
lemmas iszero_(h)complex_number_of are no longer needed
|
file |
diff |
annotate
|
| Wed, 09 May 2007 18:26:40 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Wed, 09 May 2007 01:26:04 +0200 |
huffman |
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
|
file |
diff |
annotate
|
| Tue, 08 May 2007 05:06:54 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 01:06:12 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Sat, 16 Dec 2006 19:37:07 +0100 |
huffman |
hypreal_of_hypnat abbreviates more general of_hypnat
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 19:15:16 +0100 |
huffman |
generalized type of hyperpow; removed hcpow
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 18:10:38 +0100 |
huffman |
redefine hSuc as *f* Suc, and move to HyperNat.thy
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 21:25:56 +0100 |
huffman |
added lemmas about hRe, hIm, HComplex; removed all uses of star_n
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 07:09:19 +0200 |
huffman |
hypreal_of_nat abbreviates of_nat
|
file |
diff |
annotate
|
| Wed, 27 Sep 2006 05:19:24 +0200 |
huffman |
convert more proofs to transfer principle
|
file |
diff |
annotate
|