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
Sat, 16 Sep 2006 02:40:00 +0200 generalized types of many constants to work over arbitrary vector spaces;
huffman [Sat, 16 Sep 2006 02:40:00 +0200] rev 20552
generalized types of many constants to work over arbitrary vector spaces; modified theorems using Rep_star to eliminate existential quantifiers
Sat, 16 Sep 2006 02:35:58 +0200 add theorem norm_diff_triangle_ineq
huffman [Sat, 16 Sep 2006 02:35:58 +0200] rev 20551
add theorem norm_diff_triangle_ineq
(0) -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip