src/HOL/String.thy
changeset 75556 1f6fc2416a48
parent 75398 a58718427bff
child 75622 53b61706749b