Wed, 21 Dec 2016 21:26:26 +0100 | haftmann | prefer existing logical constant over abbreviation | changeset | files |
Wed, 21 Dec 2016 21:26:26 +0100 | haftmann | dropped aliasses | changeset | files |
Wed, 21 Dec 2016 21:26:25 +0100 | haftmann | removed dangerous simp rule: prime computations can be excessively long | changeset | files |
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 |
Wed, 21 Dec 2016 12:49:15 +0100 | blanchet | generalized ML function (towards nonuniform datatypes) | changeset | files |
Wed, 21 Dec 2016 11:45:16 +0100 | blanchet | generalized ML function (towards nonuniform datatypes) | changeset | files |