| Wed, 13 Jul 2011 07:26:31 +0200 | haftmann | more generalization towards complete lattices | changeset | files |
| Wed, 13 Jul 2011 15:50:45 +0200 | krauss | experimental variants of Library/Cset.thy and Library/Dlist_Cset.thy defined via quotient package | changeset | files |
| Wed, 13 Jul 2011 04:00:32 +0900 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 13 Jul 2011 11:31:36 +0900 | Cezary Kaliszyk | Tuned | changeset | files |
| 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 |
| Wed, 13 Jul 2011 20:36:18 +0200 | wenzelm | sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); | changeset | files |