| Tue, 03 Jul 2007 21:56:25 +0200 | paulson | to handle non-atomic assumptions | changeset | files |
| Tue, 03 Jul 2007 20:26:08 +0200 | wenzelm | rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman); | changeset | files |
| Tue, 03 Jul 2007 18:42:09 +0200 | huffman | convert instance proofs to Isar style | changeset | files |
| Tue, 03 Jul 2007 18:00:57 +0200 | chaieb | Dependency on reflection_data.ML to build HOL-ex | changeset | files |