Wed, 28 Apr 2010 12:49:52 +0200 | blanchet | insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs | file | diff | annotate |
Tue, 27 Apr 2010 18:07:51 +0200 | blanchet | redid the proofs with the latest Sledgehammer; | file | diff | annotate |
Tue, 20 Oct 2009 19:52:04 +0200 | wenzelm | modernized session Metis_Examples; | file | diff | annotate | base |