src/HOL/String.thy
changeset 59400 d833cba5cce5
parent 58889 5b7a9633cfa8
child 59483 ddb73392356e
equal deleted inserted replaced
59399:47fb85ccfce8 59400:d833cba5cce5