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?
Tobias _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
