the isar/Example.thy (or an equivalent Example.v) file does not exist. I am sorry for the inconvenience, but this is not really under my control. Isabelle is not available as Debian package and the Isabelle maintainers distribute Isabelle with their own version of Proof General. Consequently, I removed all Isabelle stuff from the Debian Proof General package. If you want to do the Proof General tutorial with Isabelle, just deinstall the Debian Proof General package and use the instance that comes with Isabelle.
Alternatively, you can download an example file from the Coq website and use that for the tutorial. Bye, Hendrik -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected]
