Re: [isabelle] Theory loader: cannot update finished theory "Main"



On Thu, 28 Sep 2006, Jeremy Dawson wrote:

> > with_path "Integ" update_thy "Main";
> ### Theory loader: cannot update finished theory "Main"
> 
> When is a theory "finished"?

After finishing a session, i.e. when usedir has succefully compiled 
everything.  You can bootstrap HOL interactively like this:

  - copy HOL/ROOT.ML to HOL/root.ML
  - replace ``with_path "Integ" use_thy "Main";'' by ``add_path "Integ";''
  - delete the subsequent lines
  - start Isabelle Pure
  - issue ``use "root.ML"''

Now you can assert arbitrary theories from the HOL sources.


	Makarius







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.