src/HOL/Inequalities.thy
changeset 71042 400e9512f1d3
parent 66936 cf8d8fc23891