[isabelle-dev] Raw_Simplifier.rewrite: repeated ad-hoc construction of simpset
noschinl at in.tum.de
Thu Sep 19 17:07:07 CEST 2013
On 16.09.2013 19:08, Florian Haftmann wrote:
>>> However the current implementation of Raw_Simplifier.rewrite (see patch
>>> below) awaits a concrete application to a cterm before actually building
>>> the corresponding simpset in »the« context.
>> I see the same dynamic building of the simpset in Isabelle2013. But you
>> are right that the full absorption of the simpset into the context has
>> lead to situations that are a bit more dynamic than before, i.e. the
>> simpset is produced later when the tool is applied.
I see some effect on this in HOL-Algebra, for example UnivPoly.thy:
context UP_Ring begin
gives me a bunch of "Ignoring duplicate rewrite rule". This is the same
behaviour as before. But every lemma statement in this context has now
the same warnings.
(This is in 7613573f023a).
More information about the isabelle-dev