src/HOL/Tools/Function/pat_completeness.ML
changeset 82775 61c39a9e5415
parent 60781 2da59cdf531c