Re: [isabelle] Build HOL



I assume that when you say “class” you actually mean “Isabelle theory”.

In the manuals (Isabelle/HOL: A Proof Assistant for Higher-Order Logic or Programming and Proving in Isabelle/HOL), you should quickly reach the advice that you should base any theory that you write on the theory Main. In that case, no other theories should need to be loaded. The only other theory to adopt as a starting point is Complex_Main, which includes some analysis. It is generally a mistake to import other theories from src/HOL or to store your own theories there.

But even so, I am puzzled by your question. Isabelle/HOL pre-loads all the theories in the directory you mention, so I cannot see how they could be loaded again. I wonder whether the phenomenon you mention is simply that, when run for the first time, the system will automatically build Isabelle/HOL for you.

Another remark: Isabelle2013-1 was found to have issues and was quickly replaced by Isabelle2013-2, which I advise you to download and use instead.

Larry Paulson


On 10 Jan 2014, at 10:15, Roger H. <s57076 at hotmail.com> wrote:

> Hi,
> 
> im writing a class in the folder scr/HOL/Myclass
> 
> and everytime i open it, like 20 other classes need to be compiled.
> 
> Using jEdit, isabelle 2013-1, how do i build them, so that the compiler only needs to run through only my own class?
> 
> Thank you!
> 		 	   		  





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