src/HOL/Fun.thy
changeset 80148 b156869b826a
parent 79597 76a1c0ea6777