--- a/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Sledgehammer.thy Mon Jan 31 16:09:23 2022 +0100
@@ -35,32 +35,4 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
-(*
-lemma "1 + 1 = 2"
- sledgehammer [slices = 40, max_proofs = 40]
-
-lemma "1 + 1 = 2"
- sledgehammer [verbose, slices = 4]
- oops
-*)
-
-(*
-lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
- sledgehammer [max_proofs = 3]
- oops
-*)
-
-(*
-declare nat_induct[no_atp]
-declare nat_induct_non_zero[no_atp]
-
-lemma "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"
- sledgehammer [cvc4] (add: nat.induct)
-*)
-
-(*
-lemma "1 + 1 = 2 \<and> 0 + (x::nat) = x"
- sledgehammer [verbose, e, dont_preplay, max_facts = 2] (add_0_left one_add_one)
-*)
-
end