[isabelle-dev] is_concealed

[Dmitriy Traytel]

Sorry for reviving an ancient thread, but have the constants defined by 
inductive ever been visible to find_consts since Florian's commit (I 
presume 4a3747517552 ?).

Today in be4a911aca71 (but also in Isabelle2014 and even in 
Isabelle2012) in the following

inductive xyz :: bool where "xyz"
find_consts name: xyz
ML ‹Consts.is_concealed (Sign.consts_of @{theory}) @{const_name xyz}›

find_consts says "found nothing" and Consts.is_concealed says true.

Visibility of constants is of course also important beyond find_consts, 
e.g. for auto-completion.

Dmitriy

On 09.09.2010 09:57, Florian Haftmann wrote:
> Am 09.09.2010 09:15, schrieb Florian Haftmann:
>> Am 09.09.2010 09:02, schrieb Tobias Nipkow:
>>> Lars noticed an anomaly and Gerwin tracked it down:
>>> Command find_consts searches only for `visible' constants. Those defined
>>> by primrec and fun are visible, but those defined by inductive(_set) are
>>> concealed. It seems that the latter should be visible, too, right? If
>>> so, can somebody close to "inductive" fix that?
> Pushed.
>
> 	Florian
>
>
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141120/56cf7b60/attachment.html>