wenzelm [Tue, 03 Jul 2007 22:27:30 +0200] rev 23561
CONVERSION: handle TYPE | TERM | CTERM | THM;
wenzelm [Tue, 03 Jul 2007 22:27:27 +0200] rev 23560
proper use of ioa_package.ML;
wenzelm [Tue, 03 Jul 2007 22:27:25 +0200] rev 23559
tuned;
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);
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;
wenzelm [Tue, 03 Jul 2007 22:27:13 +0200] rev 23556
use mucke_oracle.ML only once;
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!);
wenzelm [Tue, 03 Jul 2007 22:27:08 +0200] rev 23554
proper use of function_package ML files;
wenzelm [Tue, 03 Jul 2007 22:27:05 +0200] rev 23553
use hologic.ML in basic HOL context;
tuned proofs;
paulson [Tue, 03 Jul 2007 21:56:25 +0200] rev 23552
to handle non-atomic assumptions