src/Pure/Thy/syntax.ML
changeset 2595 548f8ed89a80
parent 257 b36874cf3b0b