Wed, 04 Jul 2007 14:10:01 +0200 *** empty log message ***
nipkow [Wed, 04 Jul 2007 14:10:01 +0200] rev 23564
*** empty log message ***
Wed, 04 Jul 2007 13:56:26 +0200 simplified a proof
paulson [Wed, 04 Jul 2007 13:56:26 +0200] rev 23563
simplified a proof
Tue, 03 Jul 2007 23:00:42 +0200 tuned;
wenzelm [Tue, 03 Jul 2007 23:00:42 +0200] rev 23562
tuned;
Tue, 03 Jul 2007 22:27:30 +0200 CONVERSION: handle TYPE | TERM | CTERM | THM;
wenzelm [Tue, 03 Jul 2007 22:27:30 +0200] rev 23561
CONVERSION: handle TYPE | TERM | CTERM | THM;
Tue, 03 Jul 2007 22:27:27 +0200 proper use of ioa_package.ML;
wenzelm [Tue, 03 Jul 2007 22:27:27 +0200] rev 23560
proper use of ioa_package.ML;
Tue, 03 Jul 2007 22:27:25 +0200 tuned;
wenzelm [Tue, 03 Jul 2007 22:27:25 +0200] rev 23559
tuned;
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!);
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip