| Mon, 19 Aug 2013 14:47:47 +0200 | blanchet | add subtypes as well as features in MaSh | changeset | files |
| Mon, 19 Aug 2013 14:41:22 +0200 | blanchet | generate patterns for variables as well in MaSh (cf. HOL(y)Hammer) | changeset | files |
| Mon, 19 Aug 2013 14:26:59 +0200 | blanchet | generate deep type patterns in MaSh | changeset | files |
| Mon, 19 Aug 2013 12:05:33 +0200 | blanchet | improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success | changeset | files |
| Sun, 18 Aug 2013 23:37:38 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 18 Aug 2013 22:44:39 +0200 | wenzelm | tuned proofs; | changeset | files |
| Sun, 18 Aug 2013 20:41:47 +0200 | wenzelm | more static simpsets, which also avoids spurious warnings due to duplicate rules provided here; | changeset | files |
| Sun, 18 Aug 2013 19:59:19 +0200 | wenzelm | more symbols; | changeset | files |