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.