src/Pure/Syntax/lexicon.ML
changeset 7943 e31a3c0c2c1e
parent 7784 228283fa5de4
child 9289 be6e79d1aae0