Date: Tue 10-May-2011
Time: Tue 10:00-17:00
The aim of the tutorial is to give participants a working knowledge of formal specifications and proofs in Isabelle, with the HOL logic and both tactical proof scripts and structured Isar proofs. There will be presentations by the instructors, with interactive examples and exercises for the participants on their own laptops.
The target audience are researchers and doctoral students who want to learn about interactive theorem proving in Isabelle.
Editor.thyto be opened with Isabelle/jEdit.
concwhile holding CONTROL/COMMAND. If it looks completely different on your system, then there is something wrong with the installation.