[isabelle] Retriving induction scheme for datatype



Hi,

We are updating our tools for inductive theorem proving to Isabelle2015.

We noticed that the Datatype package has changed, and wonder what the proper way of fetching the induction theorem for a given datatype is now (working on the ML-level, as we have a tactic for automated induction).

We can get things to work by using "Old_Datatype_Data.get_info", and registering all our datatypes with "datatype_compat". However, we would obviously want to do this in the proper way intended instead.

Grateful for help on where to look!

Best,
Moa





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