src/Pure/pure.ML
changeset 7333 6cb15c6f1d9f
parent 6888 d0c68ebdabc5
child 7718 86755cc5b83c