src/Pure/General/length.scala
changeset 64681 642b6105e6f4
parent 64618 c81bd30839a6