System.Isabelle

Using Isabelle to check theory files.

Requirements:

1. A working installation of Isabelle2009-1 (http:isabelle.in.tum.de/) 2. The 'isabelle' command must be on the PATH.

Documentation

checkTheoryFile

Arguments

:: FilePath

Path to isabelle binary.

-> Maybe Int

Number of parallel thread to use while checking.

-> Int

Maximal available time in micro-seconds

-> String

Logic Image to use

-> FilePath

Path to file to be checked

-> IO (IO String, Maybe String)

If the check went through, log-file content only, otherwise also an error message.

Use Isabelle to check the correctness of a theory file.