distinctness_store : (string * thm) list ref

SYNOPSIS
Internal theorem list of distinctness theorems.

DESCRIPTION
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
Not applicable.

SEE ALSO
define_type, distinctness, extend_rectype_net, injectivity_store.