src/HOL/Library/Char_nat.thy
changeset 37380 35815ce9218a
parent 37221 9d9205e31767
child 37692 7b072f0c8bde