src/HOL/Inequalities.thy
changeset 80509 2a9abd6a164e
parent 66936 cf8d8fc23891