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
Sat, 16 Sep 2006 18:04:14 +0200 int_diff_cases moved to Integ/IntDef.thy
huffman [Sat, 16 Sep 2006 18:04:14 +0200] rev 20553
int_diff_cases moved to Integ/IntDef.thy
(0) -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip