Tue, 03 Jul 2007 22:27:19 +0200 tuned is_comb/is_binop -- avoid construction of cterms;
wenzelm [Tue, 03 Jul 2007 22:27:19 +0200] rev 23558
tuned is_comb/is_binop -- avoid construction of cterms; removed conjunction rules (cf. HOLogic.conj_XXX);
Tue, 03 Jul 2007 22:27:16 +0200 HOLogic.conj_intr/elims;
wenzelm [Tue, 03 Jul 2007 22:27:16 +0200] rev 23557
HOLogic.conj_intr/elims; removed obsolete assocd/assoc; removed dead string_of_pol; tuned;
Tue, 03 Jul 2007 22:27:13 +0200 use mucke_oracle.ML only once;
wenzelm [Tue, 03 Jul 2007 22:27:13 +0200] rev 23556
use mucke_oracle.ML only once;
Tue, 03 Jul 2007 22:27:11 +0200 assume basic HOL context for compilation (antiquotations);
wenzelm [Tue, 03 Jul 2007 22:27:11 +0200] rev 23555
assume basic HOL context for compilation (antiquotations); added dest_cTrueprop; tuned Trueprop_conv; added low-level conj_intr/elim/elis (dire need for @{rule} antiquotation!);
Tue, 03 Jul 2007 22:27:08 +0200 proper use of function_package ML files;
wenzelm [Tue, 03 Jul 2007 22:27:08 +0200] rev 23554
proper use of function_package ML files;
Tue, 03 Jul 2007 22:27:05 +0200 use hologic.ML in basic HOL context;
wenzelm [Tue, 03 Jul 2007 22:27:05 +0200] rev 23553
use hologic.ML in basic HOL context; tuned proofs;
Tue, 03 Jul 2007 21:56:25 +0200 to handle non-atomic assumptions
paulson [Tue, 03 Jul 2007 21:56:25 +0200] rev 23552
to handle non-atomic assumptions
Tue, 03 Jul 2007 20:26:08 +0200 rename class dom to ring_1_no_zero_divisors (cf. HOL/Ring_and_Field.thy 1.84 by huffman);
wenzelm [Tue, 03 Jul 2007 20:26:08 +0200] rev 23551
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 convert instance proofs to Isar style
huffman [Tue, 03 Jul 2007 18:42:09 +0200] rev 23550
convert instance proofs to Isar style
Tue, 03 Jul 2007 18:00:57 +0200 Dependency on reflection_data.ML to build HOL-ex
chaieb [Tue, 03 Jul 2007 18:00:57 +0200] rev 23549
Dependency on reflection_data.ML to build HOL-ex
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip