Re: [isabelle] addsimps with reorient?
The reasoning was that if the user explicitly adds a certain equation,
the system should not interfere. But I agree that a "safe" variant would
be useful. I talked it over with Stefan who will make something like
Holger Gast schrieb:
the Isabelle simplifier re-orients equalities
when extracting premises, such that, for instance,
equalities of the form x = t x, where x occurs on
the right hand side, become rewrite rules t x == x
to avoid looping.
Now I have a list of theorems thms
(they are actually premises extracted earlier)
which I would like to add as rewrite rules with
ss addsimps thms
Unfortunately, these re-write rules (as far as I see from
meta_simplifier.ML) do not get re-oriented, and the
theorems obtained with prems_of_ss are not re-oriented either.
Is there anything like
ss addsimps_safe thms
This archive was generated by a fusion of
Pipermail (Mailman edition) and