src/HOL/Inequalities.thy
changeset 73821 9ead8d9be3ab
parent 66936 cf8d8fc23891