Re: [isabelle] Getting an induction theorem from a type-name in an ML function

Hi Lucas,

see the recent thread ( where basically the same question has been answered already.

Hope that helps,

> On 12 Oct 2015, at 04:00, Lucas Dixon <lucas.dixon at> wrote:
> Hi,
> 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
> package?)
> Thanks!
> lucas

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.