Wed, 24 Oct 2012 18:43:25 +0200 | huffman | transfer package: more flexible handling of equality relations using is_equality predicate | changeset | files |
Wed, 24 Oct 2012 17:40:56 +0200 | nipkow | ensured that rewr_conv rule t = "t == u" literally not just modulo beta-eta | changeset | files |
Mon, 22 Oct 2012 22:47:14 +0200 | kuncar | new theorems | changeset | files |