src/HOL/Tools/Function/size.ML
changeset 53810 69e8ba502eda
parent 52788 da1fdbfebd39
child 55094 149ccaf4ae5c