--- a/src/HOL/ATP.thy Thu Nov 12 16:44:29 2020 +0100
+++ b/src/HOL/ATP.thy Thu Nov 12 17:42:15 2020 +0100
@@ -137,18 +137,4 @@
ML_file \<open>Tools/ATP/atp_problem_generate.ML\<close>
ML_file \<open>Tools/ATP/atp_proof_reconstruct.ML\<close>
-ML \<open>
-open ATP_Problem_Generate
-val _ = @{print} (type_enc_of_string Strict "mono_native")
-val _ = @{print} (type_enc_of_string Strict "mono_native_fool")
-val _ = @{print} (type_enc_of_string Strict "poly_native")
-val _ = @{print} (type_enc_of_string Strict "poly_native_fool")
-val _ = @{print} (type_enc_of_string Strict "mono_native?")
-val _ = @{print} (type_enc_of_string Strict "mono_native_fool?")
-val _ = @{print} (type_enc_of_string Strict "erased")
-(* val _ = @{print} (type_enc_of_string Strict "erased_fool") *)
-val _ = @{print} (type_enc_of_string Strict "poly_guards")
-(* val _ = @{print} (type_enc_of_string Strict "poly_guards_fool") *)
-\<close>
-
end
--- a/src/HOL/Sledgehammer.thy Thu Nov 12 16:44:29 2020 +0100
+++ b/src/HOL/Sledgehammer.thy Thu Nov 12 17:42:15 2020 +0100
@@ -33,20 +33,4 @@
ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
-lemma "\<not> P"
- sledgehammer [e, dont_slice, timeout = 1, type_enc = "mono_native_fool"] ()
- oops
-
-lemma "P (x \<or> f False) = P (f False \<or> x)"
- sledgehammer [prover = dummy_tfx, overlord] ()
- oops
-
-lemma "P (y \<or> f False) = P (f False \<or> y)"
- sledgehammer [e, overlord, type_enc = "mono_native_fool"] ()
- oops
-
-lemma "P (f True) \<Longrightarrow> P (f (x = x))"
- sledgehammer [e, dont_slice, timeout = 1, type_enc = "mono_native_fool", dont_preplay] ()
- oops
-
end