| 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 |
| Sat, 16 Sep 2006 02:32:48 +0200 | huffman | add required type annotation | changeset | files |
| Fri, 15 Sep 2006 22:56:17 +0200 | wenzelm | removed type aliases for theory/theory_ref; | changeset | files |