src/HOL/Inequalities.thy
changeset 63982 4c4049e3bad8
parent 63918 6bf55e6e0b75
child 64267 b9a1486e79be