External References

Put here some links to other documentation sources that can be useful.

• Isabelle FAQ
• What's is Main (by Tobias Nipkow) contains a list of populer datatypes and functions (i.e. there signatures) in the Main theory.
• A Proof Assistant for Higher-Order Logic (by Nipkow et al.) is an extensive tutorial to most of Isabelle's features. Find explanations for most methods, tactics, … via the index.

• For a list of pre-defined symbols in Isabelle/HOL see Appendix B of this document. Useful when the set of UNICODE characters is not available.

• Presentation of Sheet 2 can be found here.
• Presentation of Sheet 4 can be found here
• "Executing Higher Order Logics" is a paper making an overview of how to write functions on Isabelle/HOL and some performance issues. Good about it is that it has some code and goes over some concepts that we've seen in the lectures/tutorials
• Defining a non-concrete recursive type in HOL which includes sets is a report that at the beginning has some complementary information about type definition in HOL. Then it's just a bunch of theorems I didn't went through.