Thu, 28 Aug 2014 16:58:27 +0200 | blanchet | added 'skolem' method, esp. for 'obtain's generated from Z3 proofs | changeset | files |
Thu, 28 Aug 2014 16:58:26 +0200 | blanchet | tuned method description | changeset | files |
Thu, 28 Aug 2014 16:58:26 +0200 | blanchet | three-line 'obtain' format for generated Isar proofs | changeset | files |
Thu, 28 Aug 2014 15:51:50 +0200 | wenzelm | tuned; | changeset | files |
Thu, 28 Aug 2014 15:47:26 +0200 | wenzelm | more liberal embedded "text", which includes cartouches; | changeset | files |
Thu, 28 Aug 2014 13:25:12 +0200 | wenzelm | intern xthm only once; | changeset | files |