src/HOL/Tools/Function/partial_function.ML
Tue, 21 Jan 2025 19:26:39 +0100 wenzelm misc tuning: prefer specific variants of Thm.dest_comb;
less more (0) -30 -10 -1 tip