src/HOL/Inequalities.thy
changeset 82218 cbf9f856d3e0
parent 66936 cf8d8fc23891