[isabelle] addsimps with reorient?



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

Thanks,

Holger








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.