Thu, 07 Mar 2013 18:14:30 +0100avoid -Infinity which confuses JFreeChart histogram;
wenzelm [Thu, 07 Mar 2013 18:14:30 +0100] rev 52507
avoid -Infinity which confuses JFreeChart histogram;

Thu, 07 Mar 2013 17:50:26 +0100tuned proofs -- more structure, less warnings;
wenzelm [Thu, 07 Mar 2013 17:50:26 +0100] rev 52506
tuned proofs -- more structure, less warnings;

Thu, 07 Mar 2013 15:02:55 +0100tuned signature -- prefer terminology of Scala and Axiom;
wenzelm [Thu, 07 Mar 2013 15:02:55 +0100] rev 52505
tuned signature -- prefer terminology of Scala and Axiom;

Thu, 07 Mar 2013 13:44:54 +0100better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)
blanchet [Thu, 07 Mar 2013 13:44:54 +0100] rev 52504
better message (type-unsoundnesses are becoming rare, usually the issue is elsewhere, e.g. in the TSTP proof parser)

Wed, 06 Mar 2013 10:44:43 -0800avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)
huffman [Wed, 06 Mar 2013 10:44:43 -0800] rev 52503
avoid using Arith_Data.dest_sum in extended-nat simprocs (it treats 'x - y' as 'x + - y', which is not valid for enat)

Wed, 06 Mar 2013 16:56:21 +0100netlimit is abbreviation for Lim
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 52502
netlimit is abbreviation for Lim

Wed, 06 Mar 2013 16:56:21 +0100tuned proofs
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 52501
tuned proofs

Wed, 06 Mar 2013 16:56:21 +0100changed has_derivative_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 52500
changed has_derivative_intros into a named theorems collection

Wed, 06 Mar 2013 16:56:21 +0100changed continuous_on_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 52499
changed continuous_on_intros into a named theorems collection

Wed, 06 Mar 2013 16:56:21 +0100changed continuous_intros into a named theorems collection
hoelzl [Wed, 06 Mar 2013 16:56:21 +0100] rev 52498
changed continuous_intros into a named theorems collection