doc-src/Tutorial/Misc/exhaust.ML
changeset 13300 debf9ef73e4e
parent 9255 2ceb11a2e190