wenzelm [Thu, 05 Jul 2007 00:15:44 +0200] rev 23587
tuned;
wenzelm [Thu, 05 Jul 2007 00:06:25 +0200] rev 23586
avoid polymorphic equality;
added dest_judgment;
wenzelm [Thu, 05 Jul 2007 00:06:24 +0200] rev 23585
sort_le: tuned eq case;
wenzelm [Thu, 05 Jul 2007 00:06:23 +0200] rev 23584
tuned goal conversion interfaces;
wenzelm [Thu, 05 Jul 2007 00:06:22 +0200] rev 23583
else_conv: only handle THM | CTERM | TERM | TYPE;
prems_conv: no index;
renamed goal_conv_rule to gconv_rule;
wenzelm [Thu, 05 Jul 2007 00:06:20 +0200] rev 23582
avoid polymorphic equality;
Numeral.mk_cnumber;
wenzelm [Thu, 05 Jul 2007 00:06:19 +0200] rev 23581
tuned;
wenzelm [Thu, 05 Jul 2007 00:06:18 +0200] rev 23580
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
tuned;
wenzelm [Thu, 05 Jul 2007 00:06:17 +0200] rev 23579
avoid polymorphic equality;
do not export ring_conv (which is not a conversion anyway);
renamed algebra_tac to ring_tac;
ring_tac: simplified tactic wrapper, no longer handles ERROR;
wenzelm [Thu, 05 Jul 2007 00:06:16 +0200] rev 23578
avoid polymorphic equality;
removed dead code;