Mon, 23 Sep 2019 17:15:29 +0200 | nipkow | Enforced precodition "n <= length xs" to avoid relying on "hd []". | changeset | files |
Mon, 23 Sep 2019 14:08:49 +0100 | paulson | Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous) | changeset | files |