src/HOL/Inequalities.thy
changeset 70213 ff8386fc191d
parent 66936 cf8d8fc23891