[isabelle] Isabelle/HOL 2005



Dear all,

I am reviewing a paper which includes an Isabelle/HOL 2005
formalization and I want to verify the formalization myself. The
formalization consists of six files xxx.{thy,ML}, yyy.{thy,ML} and
zzz.{thy,ML}. I have no prior experience with the Isabelle proof
assistant.

Three questions:

- How do I install Isabelle/HOL 2005 and use it to verify the
formalization? My available platforms are OS X and Linux.

- My background in interactive theorem proving is with Coq. In Coq one
can add additional axioms in one's formalization. Can one do something
similar in Isabelle/HOL and if so how do I check what (if any) axioms
have been added? (That is, how do I check that the authors of the
paper have not "cheated" in their proofs.)

- Anything else I should think of?

Best regards,

Anonymous Reviewer




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