| Thu, 10 May 2007 03:07:26 +0200 | huffman | lemmas iszero_(h)complex_number_of are no longer needed | changeset | files |
| Thu, 10 May 2007 03:00:15 +0200 | huffman | instance real_algebra_1 < ring_char_0 | changeset | files |
| Thu, 10 May 2007 02:51:53 +0200 | huffman | new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas | changeset | files |
| Thu, 10 May 2007 00:39:56 +0200 | wenzelm | moved conversions to structure Conv; | changeset | files |
| Thu, 10 May 2007 00:39:55 +0200 | wenzelm | added dest_fun/fun2/arg1; | changeset | files |
| Thu, 10 May 2007 00:39:54 +0200 | wenzelm | tuned argument_type_of; | changeset | files |
| Thu, 10 May 2007 00:39:53 +0200 | wenzelm | added destructors from drule.ML; | changeset | files |
| Thu, 10 May 2007 00:39:52 +0200 | wenzelm | moved some operations to more_thm.ML and conv.ML; | changeset | files |