src/HOL/Lex/Prefix.thy
changeset 7304 94c6f8f07631
parent 6675 63e53327f5e5
child 8523 7ffc94f2f42d