isabelle: Changelog

wenzelm [Tue, 19 Jun 2007 23:15:38 +0200] rev 23419

BalancedTree;

wenzelm [Tue, 19 Jun 2007 23:15:27 +0200] rev 23418

balanced conjunctions;

wenzelm [Tue, 19 Jun 2007 23:15:23 +0200] rev 23417

tuned;

krauss [Tue, 19 Jun 2007 18:00:49 +0200] rev 23416

generalized proofs so that call graphs can have any node type.

wenzelm [Tue, 19 Jun 2007 00:02:16 +0200] rev 23415

macbroy5: trying -j 2;

wenzelm [Mon, 18 Jun 2007 23:30:46 +0200] rev 23414

tuned conjunction tactics: slightly smaller proof terms;

nipkow [Sun, 17 Jun 2007 18:47:03 +0200] rev 23413

tuned laws for cancellation in divisions for fields.

chaieb [Sun, 17 Jun 2007 13:39:50 +0200] rev 23412

moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs

chaieb [Sun, 17 Jun 2007 13:39:48 +0200] rev 23411

Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl

chaieb [Sun, 17 Jun 2007 13:39:45 +0200] rev 23410

gen_qelim_conv now reduces the universal quatifier to the existential one; Now also deals with Ex f for eta-contracted f;

isabelle