src/Pure/section_utils.ML
changeset 7535 599d3414b51d
parent 6390 5d58c100ca3f
child 7744 f27d54c1ef39
equal deleted inserted replaced
7534:30344dde83ab 7535:599d3414b51d