| Sat, 16 Sep 2006 23:46:38 +0200 | huffman | complex_of_real abbreviates of_real::real=>complex; | changeset | files |
| Sat, 16 Sep 2006 19:14:37 +0200 | huffman | add instance for real_algebra_1 and real_normed_div_algebra | changeset | files |
| Sat, 16 Sep 2006 19:12:54 +0200 | huffman | add instances for real_vector and real_algebra | changeset | files |
| Sat, 16 Sep 2006 19:12:03 +0200 | huffman | define new constant of_real for class real_algebra_1; | changeset | files |
| Sat, 16 Sep 2006 18:04:14 +0200 | huffman | int_diff_cases moved to Integ/IntDef.thy | changeset | files |
| Sat, 16 Sep 2006 02:40:00 +0200 | huffman | generalized types of many constants to work over arbitrary vector spaces; | changeset | files |
| Sat, 16 Sep 2006 02:35:58 +0200 | huffman | add theorem norm_diff_triangle_ineq | changeset | files |