src/Pure/section_utils.ML
changeset 949 83c588d6fee9
parent 654 65435e2c6512
child 1390 bf523422a3df
equal deleted inserted replaced
948:3647161d15d3 949:83c588d6fee9