src/Pure/more_pattern.ML
changeset 82648 35e40c60c680
parent 81253 bbed9f218158