src/HOL/Library/Char_nat.thy
changeset 30510 4120fc59dd85
parent 30224 79136ce06bdb
child 30663 0b6aff7451b2
equal deleted inserted replaced
30509:e19d5b459a61 30510:4120fc59dd85