src/Pure/Syntax/syntax.ML
changeset 44197 458573968568
parent 44113 0baa8bbd355a
child 44802 65c397cc44ec