src/HOL/Library/Code_Binary_Nat.thy
changeset 82775 61c39a9e5415
parent 82774 2865a6618cba