Slides
The slides will be made avaiable during the semester.
- Organization, Introduction, Higher-Order Logic (4 on 1) and Demo01.thy
- Pure Framework, Structured Proofs (4 on 1) and Demo02.thy
- Structured Proofs Continued, Case Analysis and Induction (4 on 1) and Demo03.thy
- Induction Revisited, Calculation Reasoning, Simplifier (4 on 1) and Demo04.thy
- Function Definitions Revisited, Manual Termination Proofs, Attributes (4 on 1) and Demo05.thy
- Projects, Proof Methods, Sledgehammer (4 on 1) and Demo06.thy
- Inductive Definitions, Rule Inversion and Induction (4 on 1) and Demo07.thy
- Sets and Lists in Isabelle, Case Study: Binary Search Trees (4 on 1) and Demo08.thy (Demo08_completed.thy)
- Typedef, Lifting and Transfer (4 on 1) and Demo09.thy
- Code Generation – Part 1 (4 on 1) and Demo10.thy
- Code Generation – Part 2 (4 on 1) and Demo11.thy
- Sessions, Document Preparation, Type Classes (4 on 1) and Demo12.thy and session12.tgz
- Further Topics, Master Projects (4 on 1) and Demo13.thy