| Tue, 30 Sep 2014 11:19:30 +0200 | blanchet | tuning | changeset | files |
| Tue, 30 Sep 2014 11:06:26 +0200 | blanchet | keep rules with no premises in Isar proofs from veriT | changeset | files |
| Tue, 30 Sep 2014 10:25:04 +0200 | blanchet | correct indexing in the presence of lambda-lifting | changeset | files |
| Mon, 29 Sep 2014 22:09:17 +0200 | nipkow | merged | changeset | files |
| Mon, 29 Sep 2014 22:09:05 +0200 | nipkow | tuned | changeset | files |
| Mon, 29 Sep 2014 21:40:02 +0200 | blanchet | merge | changeset | files |
| Mon, 29 Sep 2014 20:26:04 +0200 | blanchet | support hypotheses with schematics in Isar proofs | changeset | files |
| Mon, 29 Sep 2014 21:34:48 +0200 | nipkow | tuned | changeset | files |
| Mon, 29 Sep 2014 18:37:33 +0200 | blanchet | simplified and repaired veriT index handling code | changeset | files |
| Mon, 29 Sep 2014 14:32:30 +0200 | blanchet | made 'moura' tactic more powerful | changeset | files |
| Mon, 29 Sep 2014 12:30:12 +0200 | blanchet | fixed wrong optimization (wrong because it may affect the sequent's conclusion) | changeset | files |
| Mon, 29 Sep 2014 12:30:09 +0200 | blanchet | merge | changeset | files |
| Mon, 29 Sep 2014 12:29:52 +0200 | blanchet | added option to get cleaner SPASS proofs | changeset | files |
| Mon, 29 Sep 2014 10:39:39 +0200 | blanchet | parse back type of SPASS proof variables | changeset | files |
| Mon, 29 Sep 2014 10:39:39 +0200 | blanchet | make sure no '__' suffixes make it until Isar proof | changeset | files |
| Mon, 29 Sep 2014 10:39:39 +0200 | blanchet | rename skolem symbols in the negative case as well | changeset | files |
| Mon, 29 Sep 2014 10:39:39 +0200 | blanchet | reintroduced 'rel_cases' in docs | changeset | files |
| Mon, 29 Sep 2014 10:39:39 +0200 | blanchet | added options to Mirabelle | changeset | files |
| Mon, 29 Sep 2014 10:39:39 +0200 | blanchet | tuning | changeset | files |
| Mon, 29 Sep 2014 11:18:25 +0200 | wenzelm | faster machine for slow/bulky polyml-5.3.0 tests (notably HOL-Proofs); | changeset | files |
| Mon, 29 Sep 2014 09:57:34 +0200 | wenzelm | pro-forma support for polyml-5.5.3 (presently SVN 1960); | changeset | files |
| Mon, 29 Sep 2014 08:13:23 +0200 | haftmann | corrected white-space accident | changeset | files |
| Sun, 28 Sep 2014 20:27:47 +0200 | haftmann | tuned | changeset | files |
| Sun, 28 Sep 2014 20:27:46 +0200 | haftmann | moved to HOL and generalized | changeset | files |
| Fri, 26 Sep 2014 19:38:26 +0200 | wenzelm | merged | changeset | files |
| Fri, 26 Sep 2014 15:10:02 +0200 | wenzelm | proper range for Antiq tokens; | changeset | files |
| Fri, 26 Sep 2014 15:05:11 +0200 | wenzelm | support for sub-expression markup; | changeset | files |
| Fri, 26 Sep 2014 14:29:06 +0200 | wenzelm | tuned message; | changeset | files |
| Fri, 26 Sep 2014 14:43:28 +0200 | desharna | refactor fp_sugar move theorems | changeset | files |
| Fri, 26 Sep 2014 14:43:26 +0200 | desharna | refactor fp_sugar move theorems | changeset | files |
| Fri, 26 Sep 2014 14:41:54 +0200 | desharna | refactor fp_sugar move theorems | changeset | files |
| Fri, 26 Sep 2014 14:41:15 +0200 | desharna | refactor fp_sugar move theorems | changeset | files |
| Fri, 26 Sep 2014 14:41:08 +0200 | desharna | refactor fp_sugar move theorems | changeset | files |
| Fri, 26 Sep 2014 14:36:54 +0200 | desharna | refactor fp_sugar with empty substructures | changeset | files |
| Fri, 26 Sep 2014 14:35:09 +0200 | desharna | add attribute 'case_names' to 'set_case' | changeset | files |
| Fri, 26 Sep 2014 09:58:35 +0200 | desharna | make 'case_transfer' tactic more robust | changeset | files |
| Thu, 25 Sep 2014 18:47:32 +0200 | haftmann | more correct precedence of do-notation | changeset | files |
| Thu, 25 Sep 2014 17:07:44 +0200 | wenzelm | merged | changeset | files |
| Thu, 25 Sep 2014 15:01:42 +0200 | wenzelm | save image as PNG or PDF; | changeset | files |
| Thu, 25 Sep 2014 12:22:12 +0200 | wenzelm | support for PNG output; | changeset | files |
| Thu, 25 Sep 2014 10:36:39 +0200 | wenzelm | more isatests (on lxbroy4); | changeset | files |
| Thu, 25 Sep 2014 16:35:56 +0200 | desharna | document 'corec_transfer' | changeset | files |
| Thu, 25 Sep 2014 16:35:56 +0200 | desharna | generate 'corec_transfer' for codatatypes | changeset | files |
| Thu, 25 Sep 2014 16:35:54 +0200 | desharna | document 'rec_transfer' | changeset | files |
| Thu, 25 Sep 2014 16:35:53 +0200 | desharna | generate 'rec_transfer' for datatypes | changeset | files |
| Thu, 25 Sep 2014 16:35:51 +0200 | desharna | generate 'dtor_corec_transfer' for codatatypes | changeset | files |
| Thu, 25 Sep 2014 16:35:50 +0200 | desharna | generate 'ctor_rec_transfer' for datatypes | changeset | files |
| Mon, 01 Sep 2014 14:14:47 +0200 | traytel | goal generation for xtor_co_rec_transfer | changeset | files |
| Thu, 25 Sep 2014 13:30:57 +0200 | blanchet | commented out some tests that require external tools (e.g. ghc) | changeset | files |
| Thu, 25 Sep 2014 13:30:57 +0200 | blanchet | added useful options to CVC4 | changeset | files |
| Thu, 25 Sep 2014 12:27:34 +0200 | traytel | subscribe for isatest | changeset | files |
| Thu, 25 Sep 2014 09:01:14 +0200 | traytel | even more deads go to the end (continuation of e3a01b73579f) | changeset | files |
| Thu, 25 Sep 2014 11:38:56 +0200 | nipkow | added function size1 | changeset | files |
| Wed, 24 Sep 2014 19:11:21 +0200 | haftmann | added lemmas | changeset | files |
| Wed, 24 Sep 2014 19:10:30 +0200 | haftmann | tuned | changeset | files |
| Wed, 24 Sep 2014 21:00:07 +0200 | blanchet | avoid type variable name clash | changeset | files |
| Wed, 24 Sep 2014 21:00:07 +0200 | blanchet | tuning | changeset | files |
| Wed, 24 Sep 2014 17:33:53 +0200 | blanchet | made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow | changeset | files |
| Wed, 24 Sep 2014 16:35:42 +0200 | blanchet | improved 'bnf' parser | changeset | files |
| Wed, 24 Sep 2014 15:46:41 +0200 | blanchet | updated SMT certificates | changeset | files |