src/Pure/Syntax/lexicon.ML
changeset 42224 578a51fae383
parent 42053 006095137a81
child 42264 b6c1b0c4c511