[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

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




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