src/HOL/Inequalities.thy
changeset 78646 fff610f1a6f4
parent 66936 cf8d8fc23891