src/HOL/Library/Code_Integer.thy
changeset 29868 787349bb53e9
parent 28562 4e74209f113e
child 29936 d3dfb67f0f59