/src/HOL/Tools/Sledgehammer/
drwxr-xr-x [up]
-rw-r--r-- 2025-03-18 21:39 +0000 5916 async_manager_legacy.ML
-rw-r--r-- 2025-03-18 21:39 +0000 27841 sledgehammer.ML
-rw-r--r-- 2025-03-18 21:39 +0000 46170 sledgehammer_atp_systems.ML
-rw-r--r-- 2025-03-18 21:39 +0000 16198 sledgehammer_commands.ML
-rw-r--r-- 2025-03-18 21:39 +0000 22826 sledgehammer_fact.ML
-rw-r--r-- 2025-03-18 21:39 +0000 3802 sledgehammer_instantiations.ML
-rw-r--r-- 2025-03-18 21:39 +0000 24045 sledgehammer_isar.ML
-rw-r--r-- 2025-03-18 21:39 +0000 6639 sledgehammer_isar_annotate.ML
-rw-r--r-- 2025-03-18 21:39 +0000 14661 sledgehammer_isar_compress.ML
-rw-r--r-- 2025-03-18 21:39 +0000 5911 sledgehammer_isar_minimize.ML
-rw-r--r-- 2025-03-18 21:39 +0000 9535 sledgehammer_isar_preplay.ML
-rw-r--r-- 2025-03-18 21:39 +0000 17531 sledgehammer_isar_proof.ML
-rw-r--r-- 2025-03-18 21:39 +0000 61868 sledgehammer_mash.ML
-rw-r--r-- 2025-03-18 21:39 +0000 23149 sledgehammer_mepo.ML
-rw-r--r-- 2025-03-18 21:39 +0000 9045 sledgehammer_proof_methods.ML
-rw-r--r-- 2025-03-18 21:39 +0000 10606 sledgehammer_prover.ML
-rw-r--r-- 2025-03-18 21:39 +0000 17125 sledgehammer_prover_atp.ML
-rw-r--r-- 2025-03-18 21:39 +0000 11942 sledgehammer_prover_minimize.ML
-rw-r--r-- 2025-03-18 21:39 +0000 6823 sledgehammer_prover_smt.ML
-rw-r--r-- 2025-03-18 21:39 +0000 4365 sledgehammer_prover_tactic.ML
-rw-r--r-- 2025-03-18 21:39 +0000 2891 sledgehammer_tactics.ML
-rw-r--r-- 2025-03-18 21:39 +0000 5298 sledgehammer_util.ML