Thu, 07 Apr 2016 17:20:21 +0200 | wenzelm | updated documentation; | changeset | files |
Thu, 07 Apr 2016 16:53:43 +0200 | wenzelm | more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; | changeset | files |
Thu, 07 Apr 2016 15:32:47 +0200 | wenzelm | unused (see caaa2fc4040d); | changeset | files |
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 |