Tue, 20 Dec 2016 15:39:13 +0100 | haftmann | emphasize dedicated rewrite rules for congruences | changeset | files |
Wed, 21 Dec 2016 17:37:58 +0100 | blanchet | moved and exported tactic | changeset | files |
Wed, 21 Dec 2016 13:35:58 +0100 | blanchet | export ML function (towards nonuniform datatypes) | changeset | files |