Thu, 13 Mar 2014 14:48:20 +0100 | blanchet | added 'smt2_status' to keywords | changeset | files |
Thu, 13 Mar 2014 14:48:20 +0100 | blanchet | avoid name clash | changeset | files |
Thu, 13 Mar 2014 14:48:20 +0100 | blanchet | simplify index handling | changeset | files |
Thu, 13 Mar 2014 14:48:20 +0100 | blanchet | more robust indices | changeset | files |
Thu, 13 Mar 2014 14:48:20 +0100 | blanchet | correctly reconstruct helper facts (e.g. 'nat_int') in Isar proofs | changeset | files |
Thu, 13 Mar 2014 14:48:20 +0100 | blanchet | move lemmas to theory file, towards textual proof reconstruction | changeset | files |
Thu, 13 Mar 2014 14:48:05 +0100 | blanchet | simpler translation of 'div' and 'mod' for Z3 | changeset | files |
Thu, 13 Mar 2014 13:18:14 +0100 | blanchet | tuning | changeset | files |