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

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 Li
PhD Candidate
Computer Laboratory
University of Cambridge

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