A related question: some time back I was looking at how datatypes are
constructed, and found stuff in theory ind_type, and theorems like
list_TY_DEF (which one finds by doing find "ty_def")
But it seems that there are also theorems created which define the
constructors of the list datatype in
If people wanting to store these “uninteresting” theorems are happy to wrap and
unwrap the OMITs, this would be one approach.
I had been thinking of adding a
save_private_thm(name, privatedbname, thm)
entrypoint to Theory.sml. You’d want multiple possible “private dbs”, so there
would
