src/Pure/section_utils.ML
changeset 8771 026f37a86ea7
parent 7744 f27d54c1ef39
equal deleted inserted replaced
8770:bfab4d4b7516 8771:026f37a86ea7