Re: [isabelle] function internals in Isabelle2016-RC1
from the news file of Isabelle2016-RC1, one can see that the function internals are by default
now hidden, and only available if the functions are defined via [[function_internals]].
This is perfectly fine, however I encountered the problem that not ALL function internals are exposed,
e.g., when defining f, one sees both f_def and f_sumC_def as expected. However, at least in some formalization I also
need to access f_graph_def which is no longer made available, even if [[function_internals]] is enabled.
Is there any reason for always hiding _graph_def, or can it be made available again?
This archive was generated by a fusion of
Pipermail (Mailman edition) and