Tue, 03 Jul 2007 22:27:08 +0200 | wenzelm | proper use of function_package ML files; | changeset | files |
Tue, 03 Jul 2007 22:27:05 +0200 | wenzelm | use hologic.ML in basic HOL context; | changeset | files |
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 |