User Tools

Site Tools


External References

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

  • 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.
references.txt · Last modified: 2011/05/28 17:26 by