injectivity_store : (string * thm) list ref
Internal theorem list of injectivity theorems.
This list contains all the injectivity theorems (see injectivity) for the
recursive types defined so far. It is automatically extended by define_type
and used as a cache by injectivity.
- FAILURE CONDITIONS
- SEE ALSO
define_type, distinctness_store, extend_rectype_net, injectivity.