src/Pure/Syntax/source.ML
changeset 5975 cd19eaa90f45
parent 5943 576a7f5e5e39
child 5988 1a2285f3db47