src/HOL/Lex/RegSet.thy
changeset 13145 59bc43b51aa2
parent 8732 aef229ca5e77
child 14431 ade3d26e0caf