# HG changeset patch
# User desharna
# Date 1605199335 -3600
# Node ID 914f1f98839ce73812119ef097b1c2c531e95e28
# Parent  b6b6248d4719754b659716857d571c26f068a067
Removed development code wrongfully committed

diff -r b6b6248d4719 -r 914f1f98839c src/HOL/ATP.thy
--- 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
diff -r b6b6248d4719 -r 914f1f98839c src/HOL/Sledgehammer.thy
--- 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