wenzelm [Tue, 19 Jun 2007 23:15:57 +0200] rev 23425
added raw_tactic;
wenzelm [Tue, 19 Jun 2007 23:15:54 +0200] rev 23424
moved balanced tree operations to General/balanced_tree.ML;
wenzelm [Tue, 19 Jun 2007 23:15:51 +0200] rev 23423
added with_subgoal;
wenzelm [Tue, 19 Jun 2007 23:15:49 +0200] rev 23422
balanced conjunctions;
tuned interfaces;
tuned;
wenzelm [Tue, 19 Jun 2007 23:15:47 +0200] rev 23421
balanced conjunctions;
added split_defined (from conjunction.ML);
wenzelm [Tue, 19 Jun 2007 23:15:43 +0200] rev 23420
added General/balanced_tree.ML;
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