| Sat, 31 Dec 2011 10:15:53 +0100 | krauss | disabled failing sledgehammer unit test (collateral damage of 184d36538e51) | changeset | files |
| Sat, 31 Dec 2011 00:19:32 +0100 | krauss | disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5) | changeset | files |
| Fri, 30 Dec 2011 18:14:56 +0100 | berghofe | merged | changeset | files |
| Fri, 30 Dec 2011 18:12:00 +0100 | berghofe | Made gen_dest_case more robust against eta contraction | changeset | files |
| Fri, 30 Dec 2011 17:45:13 +0100 | wenzelm | merged | changeset | files |
| Fri, 30 Dec 2011 11:11:57 +0100 | huffman | remove unnecessary intermediate lemmas | changeset | files |
| Fri, 30 Dec 2011 17:40:30 +0100 | wenzelm | tuned; | changeset | files |
| Fri, 30 Dec 2011 16:43:46 +0100 | wenzelm | eliminated old-fashioned Global_Theory.add_thms; | changeset | files |
| Fri, 30 Dec 2011 15:43:07 +0100 | wenzelm | simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac; | changeset | files |
| Fri, 30 Dec 2011 14:19:58 +0100 | wenzelm | simplified proof; | changeset | files |
| Fri, 30 Dec 2011 13:52:07 +0100 | wenzelm | simplified proof; | changeset | files |
| Fri, 30 Dec 2011 12:54:55 +0100 | wenzelm | simplified proof; | changeset | files |
| Fri, 30 Dec 2011 12:12:16 +0100 | wenzelm | more parallelism; | changeset | files |
| Fri, 30 Dec 2011 12:00:10 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 29 Dec 2011 20:32:59 +0100 | wenzelm | merged | changeset | files |
| Thu, 29 Dec 2011 20:31:58 +0100 | wenzelm | tuned -- afford slightly larger simpset in simp_defs_tac; | changeset | files |
| Thu, 29 Dec 2011 20:05:53 +0100 | wenzelm | tuned -- standard proofs by default; | changeset | files |
| Thu, 29 Dec 2011 19:37:24 +0100 | wenzelm | do not fork skipped proofs; | changeset | files |
| Thu, 29 Dec 2011 18:27:17 +0100 | wenzelm | clarified timeit_msg; | changeset | files |
| Thu, 29 Dec 2011 16:58:19 +0100 | wenzelm | tuned; | changeset | files |
| Thu, 29 Dec 2011 15:54:37 +0100 | wenzelm | comments; | changeset | files |
| Thu, 29 Dec 2011 18:54:07 +0100 | huffman | remove constant 'ccpo.lub', re-use constant 'Sup' instead | changeset | files |
| Thu, 29 Dec 2011 17:43:54 +0100 | nipkow | merged | changeset | files |
| Thu, 29 Dec 2011 17:43:40 +0100 | nipkow | tuned | changeset | files |
| Thu, 29 Dec 2011 15:14:44 +0100 | haftmann | conversions from sets to predicates and vice versa; extensionality on predicates | changeset | files |
| Thu, 29 Dec 2011 15:14:44 +0100 | haftmann | added implementation of pred_of_set | changeset | files |
| Thu, 29 Dec 2011 14:23:40 +0100 | haftmann | fundamental theorems on Set.bind | changeset | files |
| Thu, 29 Dec 2011 14:44:44 +0100 | wenzelm | updated generated files; | changeset | files |