Re: [isabelle] Getting an induction theorem from a type-name in an ML function
see the recent thread (https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-September/msg00180.html) where basically the same question has been answered already.
Hope that helps,
> On 12 Oct 2015, at 04:00, Lucas Dixon <lucas.dixon at gmail.com> wrote:
> I'm trying to update and clean up some old IsaPlanner code (last updated
> long before the new datatype package!).
> I used to use something like this `Datatype.get_info some_datatype_name`.
> But I want to move to using the new datatype package, and so
> `Old_Datatype_Data.get_info some_datatype_name` will now return NONE.
> So, what's the best way, in an ML function, given a string value for a
> type-name (found by examining the underlying term's free variables) to
> lookup an induction theorem that the datatype package generated? (where
> should I look for an ML interface for working with the new datatype
This archive was generated by a fusion of
Pipermail (Mailman edition) and