src/HOL/Lex/RegExp.thy
changeset 7990 0a604b2fc2b1
parent 5184 9b8547a9496a
child 11379 0c90ffd3f3e2