src/HOL/Library/Code_Integer.thy
changeset 43244 db041e88a805
parent 39272 0b61951d2682
child 47108 2a1953f0d20d
equal deleted inserted replaced
43243:a59b126c72ef 43244:db041e88a805