src/HOL/String.thy
changeset 67872 39b27d38a54c
parent 67730 f91c437f6f68
child 68028 1f9f973eed2a