Fri, 04 Nov 2011 13:52:19 +0100 | wenzelm | merged | changeset | files |
Fri, 04 Nov 2011 08:19:24 +0100 | huffman | ex/Tree23.thy: automate proof of gfull_add | changeset | files |
Fri, 04 Nov 2011 08:00:48 +0100 | huffman | ex/Tree23.thy: simplify proof of bal_del0 | changeset | files |
Fri, 04 Nov 2011 07:37:37 +0100 | huffman | ex/Tree23.thy: simplify proof of bal_add0 | changeset | files |
Fri, 04 Nov 2011 07:04:34 +0100 | huffman | ex/Tree23.thy: simpler definition of ordered-ness predicate | changeset | files |
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 |