Installing Isabelle Theorem Prover

Introduction to Isabelle [ref: wikipedia, York University],

The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory 

Isabelle consists of two components: the proof engine and user interface.

Isabelle has several interfaces available:

• Proof General (emacs) [included] 
• PIDE (jEdit) [included]
• I3P (Netbeans) 

I just started using isabelle 3 weeks ago and according to advice from Simon Foster I'm sticking with Emacs interface for now.

Download Isabelle

Some Shortcuts in Emacs

Ctrl C + N  -> next line in proof checking

Ctrl C + U -> previous line in proof checking

Ctrl C + Ctrl Enter -> go to position

Ctrl C + A + S -> sledge hammer