Dear all,
in Isabelle 2016, certain traditional interfaces to data-type packages
do no longer exist, for example Datatype.get_info thy typename or
its homologue on records. This function yielded for a given typename
the list of constructors together with their types, and other information.
This change is, as I assume, a consequence of the new layer of type-related
packages of more recent isabelle versions.
One can, of course, extract this information from the type-exhaustion schemes.
Is there another recommended way ?
By the way, the necessary pre-requisite for doing this would be to have access
to the “fast reference” operation:
ML_Thms.thm_binding kind is_single thms txt
which is at the moment not exported.
Again, what is the recommended way of doing this
(searching for a theorem in a local or global context) by its long name ?
[And please, don’t tell me it’s Eisbach.]
Best regards,
bu
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
