src/HOL/String.thy
changeset 59387 d15a96149703
parent 58889 5b7a9633cfa8
child 59483 ddb73392356e
equal deleted inserted replaced
59386:32b162d1d9b5 59387:d15a96149703