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
--
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
