Re: [Hol-info] Share list of terms with later theories

I was thinking along these lines, yeah. Such theorems could also be stopped from appearing in the Theory.sig file. Michael On 12/1/18, 07:31, "Konrad Slind" wrote: Theorems that need to persist between sessions are most easily stored by name in theories.

Re: [Hol-info] Share list of terms with later theories

Theorems that need to persist between sessions are most easily stored by name in theories. Maybe some kind of PolyML database magic could also be used, I don't know. As far as DB searches, it wouldn't be hard to implement a refined DB search mechanism that first discarded all theorems that met