src/HOL/Lex/RegSet.thy
changeset 4935 1694e2daef8f
parent 4832 bc11b5b06f87
child 8732 aef229ca5e77