| Wed, 24 Oct 2012 18:43:25 +0200 | huffman | transfer package: add test to prevent trying to make cterms from open terms | changeset | files |
| 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 |
| Mon, 22 Oct 2012 22:24:34 +0200 | haftmann | incorporated constant chars into instantiation proof for enum; | changeset | files |
| Mon, 22 Oct 2012 19:02:36 +0200 | haftmann | close code theorems explicitly after preprocessing | changeset | files |