Re: [isabelle] function internals in Isabelle2016-RC1



Dear Makarius,

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,
RenÃ


> 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".
> 
> 
> 	Makarius



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.