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