Re: [isabelle] Sum of first n integers



> So now a more basic question
> How do I know that the proof is done?

You know that if the system is done processing and doesn't complain
(i.e. nothing is highlighted in whatever color or underlined in red).
There's also the possibility to check a theory in "batch mode" outside
of the editor. In Isabelle terminology, this is called "building a
session". Refer to Â2 in the system manual for details. A simple example
for your theory would be to create a file "ROOT" with the following
contents:

session Your_Session_Name = HOL +
  theories
    Your_Theory_Name

... and then invoking "isabelle build -v -D ." in that directory.

Cheers
Lars




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