| Wed, 28 Apr 2010 14:19:26 +0200 | blanchet | redo Sledgehammer proofs (and get rid of "neg_clausify") | changeset | files |
| Wed, 28 Apr 2010 13:32:45 +0200 | blanchet | removed "sorts" option, continued | changeset | files |
| Wed, 28 Apr 2010 13:00:30 +0200 | blanchet | remove Sledgehammer's "sorts" option to annotate variables with sorts in proof; | changeset | files |
| 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 | changeset | files |
| Wed, 28 Apr 2010 12:46:50 +0200 | blanchet | support Vampire definitions of constants as "let" constructs in Isar proofs | changeset | files |
| Tue, 27 Apr 2010 18:58:05 +0200 | blanchet | tuning | changeset | files |