On Wed, Jul 20, 2011 at 11:33 AM, Alexander Krauss <[email protected]> wrote: > Now my question is: What do we actually know when HOL-Generate-HOLLight > completes without error? Should the generated file be compared with the > version in the repository and should the test fail when they are not > identical? Are there other things that should be checked?
Completing without error is already quite good; I am not sure about the file comparison: At the moment there are two generated files, the 'thy' file and the 'imp' file. The 'thy' file has all the theorems that are present in HOL Light but not in Isabelle. The 'imp' file includes theorem mappings. If new things are proved in Isabelle that are identical to the ones that were in HOL-Light, theorems with disappear from the 'thy' file and the mapping in the 'imp' file will refer to the new theorems. This does not sound like a reason for failing? Cezary _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
