src/HOL/Library/Char_nat.thy
changeset 23024 70435ffe077d
parent 22799 ed7d53db2170
child 23394 474ff28210c0