Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Local attribute declarations Show termination ...

view this post on Zulip Email Gateway (Aug 22 2022 at 20:38):

From: Alexander Krauss <krauss@in.tum.de>
Dear all,

I just discovered that my attempt to make a local declaration does
actually do what I intended:

I wanted the [fundef_cong] declaration to affect only the following
definition, but apparrently, the declaration also affects the global
theory target.

What is the correct idiom here?

Thanks
Alex

view this post on Zulip Email Gateway (Aug 22 2022 at 20:38):

From: Peter Lammich <lammich@in.tum.de>
Hi Alex

context notes [fundef_cong] = let_unfold_cong begin

fun test ...

end

Last updated: Apr 20 2024 at 08:16 UTC