Thu, 14 Dec 2006 19:15:16 +0100 |
huffman |
generalized type of hyperpow; removed hcpow
|
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
|
Wed, 13 Dec 2006 19:05:45 +0100 |
huffman |
SComplex abbreviates Standard
|
file |
diff |
annotate
|
Wed, 27 Sep 2006 18:34:26 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|
Sun, 17 Sep 2006 02:56:25 +0200 |
huffman |
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
|
file |
diff |
annotate
|
Fri, 02 Jun 2006 23:22:29 +0200 |
wenzelm |
misc cleanup;
|
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
|
Tue, 06 Sep 2005 23:16:48 +0200 |
huffman |
replace type hypreal with real star
|
file |
diff |
annotate
|
Tue, 06 Sep 2005 20:53:27 +0200 |
huffman |
fix proof
|
file |
diff |
annotate
|
Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
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
|
Mon, 15 Mar 2004 10:58:29 +0100 |
paulson |
heavy tidying
|
file |
diff |
annotate
|
Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
Sat, 21 Feb 2004 20:05:16 +0100 |
paulson |
conversion of Complex/CStar to Isar script
|
file |
diff |
annotate
|
Mon, 05 May 2003 18:22:31 +0200 |
paulson |
new session Complex for the complex numbers
|
file |
diff |
annotate
|