src/Pure/Syntax/syn_ext.ML
changeset 5975 cd19eaa90f45
parent 5870 5d4fc952be47
child 6322 7047300264c9