src/HOL/Library/Code_Integer.thy
changeset 39214 49fc6c842d6c
parent 38857 97775f3e8722
child 39272 0b61951d2682