Re: [isabelle] function internals in Isabelle2016-RC1
thanks for the hint, it solved the problem.
According to the solution to my problem, I propose to change the NEWS-file accordingly.
Under the item for recursive function definitions where currently
only âfunction_internalsâ is mentioned, it should also list âinductive_internalsâ, because
one has to activate both options to see the real internal definition of a function.
Just my opinion,
> Am 19.01.2016 um 11:49 schrieb Makarius <makarius at sketis.net>:
> On Mon, 18 Jan 2016, Thiemann, Rene wrote:
>> I encountered the problem that not ALL function internals are exposed,
>> Is there any reason for always hiding _graph_def, or can it be made available again?
> Internals follow the internal structure of packages, so this is not "function_internals", but "inductive_internals".
This archive was generated by a fusion of
Pipermail (Mailman edition) and