the_inductive_types : (string * (thm * thm)) list ref
List of previously declared inductive types.
This reference variable contains a list of the inductive types, together with
their induction and recursion theorems as returned by define_type. The list
is automatically extended by a call of define_type.
- FAILURE CONDITIONS
- SEE ALSO