Wed, 17 Nov 2010 08:14:55 +0100 | boehmes | keep input and output files used to communicate with the SMT solver (for debugging purposes mainly) | changeset | files |
Tue, 16 Nov 2010 12:08:28 -0800 | huffman | add lemmas about powerdomains | changeset | files |
Tue, 16 Nov 2010 11:57:10 -0800 | huffman | declare {upper,lower,convex}_pd_induct as default induction rules | changeset | files |
Tue, 16 Nov 2010 11:50:05 -0800 | huffman | rename 'repdef' to 'domaindef' | changeset | files |
Wed, 17 Nov 2010 13:38:53 +0100 | wenzelm | refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text; | changeset | files |
Wed, 17 Nov 2010 11:24:07 +0100 | wenzelm | less parentheses, cf. Session.welcome; | changeset | files |