merged

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Apr 09 12:07:51 2022 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Apr 09 12:10:17 2022 +0200
@@ -2282,7 +2282,10 @@
     @{command_def (HOL) "code_identifier"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def (HOL) "code_monad"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def (HOL) "code_reflect"} & : & \<open>theory \<rightarrow> theory\<close> \\
-    @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close>
+    @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
+    @{attribute_def (HOL) code_timing} & : & \<open>attribute\<close> \\
+    @{attribute_def (HOL) code_simp_trace} & : & \<open>attribute\<close> \\
+    @{attribute_def (HOL) code_runtime_trace} & : & \<open>attribute\<close>
   \end{matharray}
 
   \<^rail>\<open>
@@ -2436,9 +2439,8 @@
 
   Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constants as arguments
   and drop all code equations declared for them. In the case of \<open>abort\<close>,
-  these constants then do not require to a specification by means of
-  code equations; if needed these are implemented by program abort (exception)
-  instead.
+  these constants if needed are implemented by program abort
+  (exception).
 
   Packages declaring code equations usually provide a reasonable default
   setup.
@@ -2502,6 +2504,15 @@
   a set of introduction rules. Optional mode annotations determine which
   arguments are supposed to be input or output. If alternative introduction
   rules are declared, one must prove a corresponding elimination rule.
+
+  \<^descr> @{attribute (HOL) "code_timing"} scrapes timing samples from different
+  stages of the code generator.
+
+  \<^descr> @{attribute (HOL) "code_simp_trace"} traces the simplifier when it is
+  used with code equations.
+
+  \<^descr> @{attribute (HOL) "code_runtime_trace"} traces ML code generated
+  dynamically for execution.
 \<close>
 
 end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Apr 09 12:07:51 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Apr 09 12:10:17 2022 +0200
@@ -171,8 +171,9 @@
 val e_config : atp_config =
   {exec = (["E_HOME"], ["eprover-ho", "eprover"]),
    arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem =>
-     ["--tstp-in --tstp-out --silent " ^ extra_options ^ " --cpu-limit=" ^
-      string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem],
+     ["--tstp-in --tstp-out --silent " ^ extra_options ^
+      " --demod-under-lambda=true --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
+      " --proof-object=1 " ^ File.bash_path problem],
    proof_delims =
      [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @
      tstp_proof_delims,

--- a/src/HOL/Tools/etc/options	Sat Apr 09 12:07:51 2022 +0200
+++ b/src/HOL/Tools/etc/options	Sat Apr 09 12:10:17 2022 +0200
@@ -32,7 +32,7 @@
 public option sledgehammer_timeout : int = 30
   -- "provers will be interrupted after this time (in seconds)"
 
-public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
+public option SystemOnTPTP : string = "https://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
   -- "URL for SystemOnTPTP service"
 
 public option MaSh : string = "sml"