src/HOL/Num.thy
changeset 47356 19fb95255ec9
parent 47300 2284a40e0f57
child 48891 c0eafbd55de3