[isabelle-dev] export_code theory wildcard exports too much
rene.neumann at in.tum.de
Fri Jun 13 17:51:38 CEST 2014
I'm currently trying to "mitigate" the changes to export_code, which
only inserts needed constants into the signature. For one theory, I
tried to use the wildcard "Theory._" -- but the then-generated code
seems to include ALL exportable definitions of some point in time. For
example, the generated code now includes the structures
Quickcheck_Exhausting and Quickcheck_Narrowing, which seems rather odd.
The documentation states "referring to all executable constants within a
certain theory by giving name._", and I thought 'within' herer refers to
'defined in', opposed to 'available in'.
> hg id
Institut für Informatik (I7)
Technische Universität München
85748 Garching b. München
Office: MI 03.11.055
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 4946 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev