src/HOL/Lex/RegSet.thy
changeset 13936 d3671b878828
parent 8732 aef229ca5e77
child 14431 ade3d26e0caf