Also worth checking out is Isabelle/HOL (another proof system): http://isabelle.in.tum.de/ http://isabelle.in.tum.de/ There are a bunch of examples in the Arch

Also worth checking out is Isabelle/HOL (another proof system): http://isabelle.in.tum.de/ http://isabelle.in.tum.de/ There are a bunch of examples in the Archive of Formal Proofs: http://afp.sourceforge.net http://afp.sourceforge.net And some tutorials: http://isabelle.in.tum.de/doc/prog-prove.pdf http://isabelle.in.tum.de/doc/prog-prove.pdf http://www-madlener.informatik.uni-kl.de/teaching/ss2011/svhol/svhol.html http://www-madlener.informatik.uni-kl.de/teaching/ss2011/svh... http://www.cse.unsw.edu.au/~cs4161/08s2/ http://www.cse.unsw.edu.au/~cs4161/08s2/