src/Pure/Isar/local_syntax.ML
changeset 24984 952045a8dcf2
parent 24960 39d1dd215d73
child 25385 42df506673ed