| Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | use metaquantification when possible in Isar proofs | changeset | files |
| Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | tuned code | changeset | files |
| Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | tuning | changeset | files |
| Wed, 31 Oct 2012 11:23:21 +0100 | blanchet | soft SMT timeout | changeset | files |
| 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 |