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

How about [simp]? Then at least simp and friends unfold it.


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.