src/HOL/HOLCF/Library/Char_Discrete.thy
changeset 62337 d3996d5873dd
parent 62175 8ffc4d0e652d
child 62597 b3f2b8c906a6