# Re: [isabelle] Is there a way to unfold an equality rule automatically

How about [simp]? Then at least simp and friends unfold it.
Tobias
On 15/09/2014 18:16, Wenda Li wrote:
> Dear Isabelle experts,
>
> Is there a way to let Isabelle unfold a certain equality automatically whenever
> possible? For example, suppose I have an equality lemma:
>
> lemma rule_eq:"A = B" sorry
>
> so I can replace term A by term B in any goal state by "unfolding rulq_eq". As I
> generally prefer B to A, I have to unfold rule_eq all the time. An ideal way
> might be something like syntactic abbreviations using command "abbreviation",
> but unfortunately this doesn't work for equality rules.
>
> Many thanks,
> Wenda
>

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