| Sun, 28 Oct 2012 02:22:39 +0000 | Christian Urban | added function store_termination_rule to the signature, as it is used in Nominal2 | changeset | files |
| Sat, 27 Oct 2012 20:59:50 +0200 | wenzelm | longer log, to accomodate final status line of isabelle build; | changeset | files |
| Wed, 24 Oct 2012 18:43:25 +0200 | huffman | transfer package: error message if preprocessing goal to object-logic formula fails | changeset | files |
| 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 |