src/HOL/Inequalities.thy
changeset 62378 85ed00c1fe7c
parent 62348 9a5f43dac883
child 63170 eae6549dbea2