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



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.