Re: [isabelle] function internals in Isabelle2016-RC1

Dear all,

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 MHonArc.