Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Is there a way to unfold an equality rule auto...

Email Gateway (Aug 19 2022 at 16:08):

From: Wenda Li <wl302@cam.ac.uk>
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

Last updated: Apr 23 2024 at 08:19 UTC