| Thu, 03 Nov 2011 17:40:50 +0100 | huffman | ex/Tree23.thy: prove that deletion preserves balance | changeset | files |
| Fri, 04 Nov 2011 00:07:45 +0100 | wenzelm | more liberal Parse.fixes, to avoid overlap of mixfix with is-pattern (notably in 'obtain' syntax); | changeset | files |
| Thu, 03 Nov 2011 23:55:53 +0100 | wenzelm | more general Proof_Context.bind_propp, which allows outer parameters; | changeset | files |