This is an old revision of the document!
External References
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.
-
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.
"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