src/HOL/Tools/Function/measure_functions.ML
changeset 79261 2e6fcc331f10
parent 67149 e61557884799
equal deleted inserted replaced
79260:f4067f14c9ed 79261:2e6fcc331f10