| Tue, 03 Jul 2007 22:27:16 +0200 | wenzelm | HOLogic.conj_intr/elims; | changeset | files |
| Tue, 03 Jul 2007 22:27:13 +0200 | wenzelm | use mucke_oracle.ML only once; | changeset | files |
| Tue, 03 Jul 2007 22:27:11 +0200 | wenzelm | assume basic HOL context for compilation (antiquotations); | changeset | files |
| 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 |