src/HOL/Tools/Function/size.ML
changeset 41417 211dbd42f95d
parent 40720 b770df486e5c
child 41423 25df154b8ffc
equal deleted inserted replaced
41414:00b2b6716ed8 41417:211dbd42f95d