src/HOL/Inequalities.thy
changeset 78564 8ba186dc9bc8
parent 66936 cf8d8fc23891