src/HOL/Library/Code_Integer.thy
changeset 29539 abfe2af6883e
parent 28562 4e74209f113e
child 29936 d3dfb67f0f59