src/HOL/Library/Code_Integer.thy
changeset 29263 bf99ccf71b7c
parent 28562 4e74209f113e
child 29936 d3dfb67f0f59