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 |