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 that available.


Holger Gast schrieb:
Dear all,

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