Thu, 14 Jul 2011 22:30:31 +0200 | wenzelm | more precise integer Markup.properties/XML.attributes: disallow ML-style ~ minus; | changeset | files |
Wed, 13 Jul 2011 22:05:55 +0200 | wenzelm | added term_sharing.ML; | changeset | files |
Wed, 13 Jul 2011 21:44:15 +0200 | wenzelm | recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck; | changeset | files |