src/HOL/SetInterval.ML
changeset 13240 bb5f4faea1f3
parent 9310 ab706fdb0842
child 13596 ee5f79b210c1