Tue, 03 Jul 2007 22:27:08 +0200 wenzelm proper use of function_package ML files;
Tue, 03 Jul 2007 22:27:05 +0200 wenzelm use hologic.ML in basic HOL context;
Tue, 03 Jul 2007 21:56:25 +0200 paulson to handle non-atomic assumptions
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);
Tue, 03 Jul 2007 18:42:09 +0200 huffman convert instance proofs to Isar style
Tue, 03 Jul 2007 18:00:57 +0200 chaieb Dependency on reflection_data.ML to build HOL-ex
(0) -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip