src/HOL/Inequalities.thy
changeset 63569 7e0b0db5e9ac
parent 63170 eae6549dbea2
child 63918 6bf55e6e0b75