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



Hi Lucas,

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,
Dmitriy


> On 12 Oct 2015, at 04:00, Lucas Dixon <lucas.dixon at gmail.com> 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.