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