src/HOL/String.thy
changeset 7007 b46ccfee8e59
parent 6395 5abd0d044adf
child 7224 e41e64476f9b