Mon, 18 Sep 2006 07:48:07 +0200 replace (x + - y) with (x - y)
huffman [Mon, 18 Sep 2006 07:48:07 +0200] rev 20563
replace (x + - y) with (x - y)
Sun, 17 Sep 2006 16:44:51 +0200 add type constraint to otherwise looping iff rule
huffman [Sun, 17 Sep 2006 16:44:51 +0200] rev 20562
add type constraint to otherwise looping iff rule
Sun, 17 Sep 2006 16:44:05 +0200 generalize type of (NS)LIM to work on functions with vector space domain types
huffman [Sun, 17 Sep 2006 16:44:05 +0200] rev 20561
generalize type of (NS)LIM to work on functions with vector space domain types
Sun, 17 Sep 2006 16:42:38 +0200 norm_one is now proved from other class axioms
huffman [Sun, 17 Sep 2006 16:42:38 +0200] rev 20560
norm_one is now proved from other class axioms
Sun, 17 Sep 2006 02:56:25 +0200 removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
huffman [Sun, 17 Sep 2006 02:56:25 +0200] rev 20559
removed capprox, CFinite, CInfinite, CInfinitesimal, cmonad, and cgalaxy in favor of polymorphic constants
Sun, 17 Sep 2006 02:53:36 +0200 hcmod abbreviates hnorm :: hcomplex => hypreal
huffman [Sun, 17 Sep 2006 02:53:36 +0200] rev 20558
hcmod abbreviates hnorm :: hcomplex => hypreal
Sat, 16 Sep 2006 23:46:38 +0200 complex_of_real abbreviates of_real::real=>complex;
huffman [Sat, 16 Sep 2006 23:46:38 +0200] rev 20557
complex_of_real abbreviates of_real::real=>complex; cmod abbreviates norm::complex=>real; removed several redundant lemmas
Sat, 16 Sep 2006 19:14:37 +0200 add instance for real_algebra_1 and real_normed_div_algebra
huffman [Sat, 16 Sep 2006 19:14:37 +0200] rev 20556
add instance for real_algebra_1 and real_normed_div_algebra
Sat, 16 Sep 2006 19:12:54 +0200 add instances for real_vector and real_algebra
huffman [Sat, 16 Sep 2006 19:12:54 +0200] rev 20555
add instances for real_vector and real_algebra
Sat, 16 Sep 2006 19:12:03 +0200 define new constant of_real for class real_algebra_1;
huffman [Sat, 16 Sep 2006 19:12:03 +0200] rev 20554
define new constant of_real for class real_algebra_1; define set Reals as range of_real; add lemmas about of_real and Reals
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip