src/HOL/Lex/RegSet.thy
changeset 12770 bdd17e7b5bd9
parent 8732 aef229ca5e77
child 14431 ade3d26e0caf