src/Pure/pure.ML
changeset 8039 a901bafe4578
parent 7718 86755cc5b83c
child 8965 d46b36785c70