isabelle: Changelog

paulson [Wed, 04 Jul 2007 13:56:26 +0200] rev 23563

simplified a proof

wenzelm [Tue, 03 Jul 2007 23:00:42 +0200] rev 23562

tuned;

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;

isabelle