src/Pure/General/completion.ML
changeset 56003 eccac152ffb4
parent 55977 ec4830499634
child 56293 9bc33476f6ac