src/HOL/Library/Code_Binary_Nat.thy
changeset 82317 231b6d8231c6
parent 81974 f30022be9213
child 82773 4ec8e654112f