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



Thanks! Moa emailed me too, that was exactly what I was looking for. cheers!

On Mon, Oct 12, 2015 at 4:53 AM Dmitriy Traytel <traytel at inf.ethz.ch> wrote:

> 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.