src/HOL/Lex/RegSet.ML
changeset 6381 ed0c7b4a325d
parent 6162 484adda70b65