[Hol-info] Theories in HOL4

[Robert M. S. <so...@Ma...>]

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