| Mon, 13 Apr 2015 14:52:40 +0200 | noschinl | rewrite: with asm pattern, try all premises for rewriting, not only the first | changeset | files |
| Mon, 13 Apr 2015 14:45:44 +0200 | noschinl | tuned | changeset | files |
| Mon, 13 Apr 2015 12:18:47 +0200 | noschinl | rewrite: propagate premises to new subgoals | changeset | files |
| Mon, 13 Apr 2015 11:58:18 +0200 | noschinl | reformat comments | changeset | files |
| Mon, 13 Apr 2015 10:39:49 +0200 | noschinl | rewr_cconv: ignore premises when tuning conclusion | changeset | files |
| Mon, 13 Apr 2015 10:21:35 +0200 | noschinl | enable \<hole> syntax for rewrite | changeset | files |
| Mon, 13 Apr 2015 13:03:41 +0200 | traytel | call Goal.prove only once for a quadratic number of theorems | changeset | files |
| Mon, 13 Apr 2015 12:15:29 +0200 | hoelzl | predicate compiler: ignore Abs_filter and Rep_filter | changeset | files |