src/HOL/Lex/RegSet.thy
changeset 13049 ce180e5b7fa0
parent 8732 aef229ca5e77
child 14431 ade3d26e0caf