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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
