|
From: Robert M. S. <so...@Ma...> - 2003-08-04 00:11:41
|
I am running HOL [Kananaskis 1]. I have some question about the use of theories. 1) How does one add a new ancestor to a theory? [What is the analogue of new_parent in HOL90?] 2) How does one save the theory created by new_theory [and the work of a session] to disk? How does one reopen the theory for further work on it in a later session. I have the documentation, so references to that would be helpful. Thank you. --Bob Solovay |