On 21/06/16 11:40, Burkhart Wolff wrote:
> 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.
Record.get_info did not change in Isabelle2016. What do you mean precisely?
The old datatype package has been superseded by BNF datatypes about 2
years ago. The BNF guys can say how to access the datatype info,
although that has changed significantly.
I somehow suspect that you are trying to move from a very old Isabelle
version to Isabelle2016, but this is a bad idea. You should always
follow each Isabelle release step by step.
> 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 ?
I don't understand that paragraph. How is this related?
> [And please, don’t tell me it’s Eisbach.]
How is this related at all?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
