src/HOL/Library/MLString.thy
changeset 21051 c49467a9c1e1
parent 20699 0cc77abb185a
child 21079 747d716e98d0