src/HOL/Lex/RegSet.thy
changeset 5936 406eb27fe53c
parent 4832 bc11b5b06f87
child 8732 aef229ca5e77