src/Pure/section_utils.ML
changeset 2160 ad4382e546fc
parent 1460 5a6f2aabd538
child 2863 d97f5f424b97
equal deleted inserted replaced
2159:e650a3f6f600 2160:ad4382e546fc