[isabelle-dev] Raw_Simplifier.rewrite: repeated ad-hoc construction of simpset

[Lars Noschinski]

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).

   -- Lars