src/HOL/Lex/Prefix.ML
changeset 6301 08245f5a436d
parent 5619 76a8c72e3fd4
child 6675 63e53327f5e5