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

• 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.