src/Pure/pure.ML
changeset 12004 1703de633aaf
parent 11761 183435fd45f2
child 12013 8d2372c6b5f3