src/HOL/Num.thy
changeset 71771 7c0de1eb6075
parent 71760 e4e05fcd8937
child 71991 8bff286878bf