src/Pure/Syntax/syntax.ML
changeset 59164 ff40c53d1af9
parent 59064 a8bcb5a446c8
child 59795 d453c69596cc