Email Gateway (Aug 23 2022 at 09:26): Email Gateway (Aug 23 2022 at 09:26):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
Hi,
I want to add the constants of a type class as terms to Generic_Data
inside the context of the class. This can be achieved using local_setup
(see the code below). Of course, the data inside the Generic_Data is
only present in the context of the class. What I want, however, is that
the data is also available in the global context with the associated
type of the type class being abstracted to a schematic type that has a
type class constraint. Apparently, this can be done using theorem
attributes (e.g. see src/HOL/Orderings.thy under the section "Reasoning
tools setup").
Is it possible to achieve the same effect without using theorem attributes?
Lukas
Last updated: Apr 24 2024 at 04:17 UTC