src/HOL/Lex/RegSet.ML
changeset 12873 d7f8dfaad46d
parent 6162 484adda70b65