src/HOL/Tools/Function/size.ML
changeset 40898 882e860a1e83
parent 40720 b770df486e5c
child 41423 25df154b8ffc
equal deleted inserted replaced
40897:1eb1b2f9d062 40898:882e860a1e83