src/Pure/Syntax/syntax.ML
changeset 59179 cad8a0012a12
parent 59064 a8bcb5a446c8
child 59795 d453c69596cc