| Mon, 16 Nov 2015 19:08:38 +0100 | haftmann | clarified contexts by factoring out reading and definition of mixins | file | diff | annotate |
| Sun, 15 Nov 2015 16:37:03 +0100 | haftmann | formally correct context for export | file | diff | annotate |
| Sun, 15 Nov 2015 10:52:51 +0100 | haftmann | tuned whitespace | file | diff | annotate |
| Sat, 14 Nov 2015 17:37:44 +0100 | haftmann | represent both algebraic and local-theory views on locale interpretation in interfaces | file | diff | annotate |
| Sat, 14 Nov 2015 08:45:52 +0100 | haftmann | tuned -- share implementations as far as appropriate | file | diff | annotate |
| Sat, 14 Nov 2015 08:45:52 +0100 | haftmann | coalesce permanent_interpretation.ML with interpretation.ML | file | diff | annotate |
| Sat, 14 Nov 2015 08:45:51 +0100 | haftmann | separate ML module for interpretation | file | diff | annotate |