src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
Wed, 12 May 2021 12:22:44 +0200 wenzelm avoid duplicate loading of ML file;
less more (0) tip