src/HOL/Num.thy
changeset 60724 4fce5d462afc
parent 59996 4dca48557921
child 60758 d8d85a8172b5