[isabelle] Retriving induction scheme for datatype
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!
This archive was generated by a fusion of
Pipermail (Mailman edition) and