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?
I am currently testing the change.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
