| 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 |
| Mon, 13 Apr 2015 12:13:52 +0200 | nipkow | merged | changeset | files |
| Mon, 13 Apr 2015 10:36:06 +0200 | nipkow | moved _aux functions from AFP/Collections to AList | changeset | files |
| Mon, 13 Apr 2015 00:59:17 +0200 | hoelzl | merged | changeset | files |