src/HOL/Lex/RegSet.ML
changeset 6980 bb526ba7ba5f
parent 6162 484adda70b65