[isabelle-dev] is_concealed

Tobias Nipkow nipkow at in.tum.de
Thu Sep 9 09:02:42 CEST 2010

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?


More information about the isabelle-dev mailing list