*To*: Holger Gast <gast at informatik.uni-tuebingen.de>*Subject*: Re: [isabelle] addsimps with reorient?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 29 Apr 2008 07:49:08 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4811B9A5.9090301@informatik.uni-tuebingen.de>*References*: <4811B9A5.9090301@informatik.uni-tuebingen.de>*User-agent*: Thunderbird 2.0.0.9 (Macintosh/20071031)

Tobias 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 Thanks, Holger

**References**:**[isabelle] addsimps with reorient?***From:*Holger Gast

- Previous by Date: [isabelle] FMCAD 2008: FINAL Call for Papers
- Next by Date: Re: [isabelle] making local definitions programmatically
- Previous by Thread: [isabelle] addsimps with reorient?
- Next by Thread: [isabelle] about the proof of ns_public_bad protocol
- Cl-isabelle-users April 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list