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