src/HOL/Lex/Prefix.thy
changeset 8039 a901bafe4578
parent 6675 63e53327f5e5
child 8523 7ffc94f2f42d