| Thu, 07 Apr 2016 13:54:02 +0200 | wenzelm | simplified default print_depth: context is usually available, in contrast to 0d295e339f52; | changeset | files |
| Thu, 07 Apr 2016 13:35:08 +0200 | wenzelm | clarified bootstrap of @{make_string} -- avoid query on ML environment; | changeset | files |
| Thu, 07 Apr 2016 12:13:11 +0200 | wenzelm | Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40); | changeset | files |