src/HOL/String.thy
changeset 57952 1a9a6dfc255f
parent 57512 cc97b347b301
child 58152 6fe60a9a5bad