| Thu, 02 Jun 2016 16:49:44 +0200 | wenzelm | eliminated pointless alias (no warning for duplicates); | changeset | files |
| Thu, 02 Jun 2016 16:23:10 +0200 | wenzelm | avoid warnings on duplicate rules in the given list; | changeset | files |
| Thu, 02 Jun 2016 15:52:45 +0200 | wenzelm | avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp; | changeset | files |