Isabelle Community Cookbook

What is this?

This repository contains the resources for the isabelle community cookbook. The cookbook contains a collection of useful tips/tricks/hints for Isabelle users.

How to contribute

If you want to add/udpdate an entry, simply add/edit the corresponding entry in the corresponding directory and create a pull request. If you need help, simply create an issue.

Build site locally

To build and view the website locally, see here.

TODO

• Add CI and html output for linked theory files (cf current Makefile)
• Move material from https://isabelle.in.tum.de/community/
• Recipes for proving existential statements
• Primer on conversions
• Latex tips
• Debugging ML code (print_tac, print antiquotation, debugger etc.)
• Overview of different tactics (should also include rewrite etc.)
• Difference between methods and tactics
• Namespacing of operators and more with bundles
• Function package tutorial
• Isabelle/jEdit FAQ. For instance: how do I get symbols to display properly?