>>> I really don’t see the gain from getting rid of sign_simps, even if
>>> it is unsuccessful. Except for the occurrence
>>>
>>> linordered_field_class.sign_simps(41)
>>>
>>> in Multivariate_Analysis/Derivative.thy.
>>
>> My primary concern is actually the comment which states that some rules
On 15/02/2015 10:32, Florian Haftmann wrote:
I really don’t see the gain from getting rid of sign_simps, even if it is
unsuccessful. Except for the occurrence
linordered_field_class.sign_simps(41)
in Multivariate_Analysis/Derivative.thy.
My primary concern is actually the comment wh
My conclusion of this discussion is that with 8fab871a2a6f the sublocale
command immediately visits its target after the qed, which it didn't before.
This now causes the command to loop. Is this correct?
Clemens
___
isabelle-dev mailing list
isabel
> I really don’t see the gain from getting rid of sign_simps, even if it is
> unsuccessful. Except for the occurrence
>
> linordered_field_class.sign_simps(41)
>
> in Multivariate_Analysis/Derivative.thy.
My primary concern is actually the comment which states that some rules
have not
