Hi, 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 8fcbfce2a2a9 tip - René -- René Neumann Institut für Informatik (I7) Technische Universität München Boltzmannstr. 3 85748 Garching b. München Tel: +49-89-289-17232 Office: MI 03.11.055
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
