src/Pure/Syntax/syn_ext.ML
changeset 5975 cd19eaa90f45
parent 5870 5d4fc952be47
child 6322 7047300264c9
equal deleted inserted replaced
5974:6acf3ff0f486 5975:cd19eaa90f45