src/HOL/Lex/Auto.ML
changeset 2919 953a47dc0519
parent 2056 93c093620c28
child 4089 96fba19bcbe2