| 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
|
| Sun, 17 Sep 2006 02:53:36 +0200 |
huffman |
hcmod abbreviates hnorm :: hcomplex => hypreal
|
file |
diff |
annotate
|
| Wed, 06 Sep 2006 13:48:02 +0200 |
haftmann |
got rid of Numeral.bin type
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
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
|
| Wed, 14 Sep 2005 01:47:06 +0200 |
huffman |
removed duplicated lemmas; convert more proofs to transfer principle
|
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
|
| Fri, 09 Sep 2005 19:34:22 +0200 |
huffman |
starfun, starset, and other functions on NS types are now polymorphic;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 01:49:49 +0200 |
huffman |
replace type hcomplex with complex star
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 00:48:50 +0200 |
huffman |
replace type hypnat with nat star
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
| Wed, 15 Dec 2004 17:32:40 +0100 |
paulson |
removal of archaic Abs/Rep proofs
|
file |
diff |
annotate
|
| Wed, 01 Sep 2004 15:04:01 +0200 |
paulson |
new "respects" syntax for quotienting
|
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
|
| Thu, 29 Jul 2004 16:14:42 +0200 |
paulson |
removed some [iff] declarations from RealDef.thy, concerning inequalities
|
file |
diff |
annotate
|