src/HOL/Lex/RegExp.thy
changeset 5936 406eb27fe53c
parent 5184 9b8547a9496a
child 11379 0c90ffd3f3e2