# HG changeset patch
# User desharna
# Date 1625749852 -7200
# Node ID 269b2f976100ab566870696aa3f1f442d8015b6c
# Parent  fa92bc604c596185a4504ab9913104b0182b70b1
added documentation for changes to Sledgehammer option "lam_trans"

diff -r fa92bc604c59 -r 269b2f976100 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jul 08 08:44:18 2021 +0200
+++ b/CONTRIBUTORS	Thu Jul 08 15:10:52 2021 +0200
@@ -6,6 +6,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* July 2021: Jasmin Blanchette and Martin Desharnais
+  Various improvements to Sledgehammer.
+
 * March 2021: Lukas Stevens
   New order prover
 
diff -r fa92bc604c59 -r 269b2f976100 NEWS
--- a/NEWS	Thu Jul 08 08:44:18 2021 +0200
+++ b/NEWS	Thu Jul 08 15:10:52 2021 +0200
@@ -192,6 +192,17 @@
 min.absorb4, max.absorb1, max.absorb2, max.absorb3, max.absorb4.  Minor
 INCOMPATIBILITY.
 
+* Sledgehammer:
+ - Removed legacy "lam_lifting" (synonym for "liftinng") from option
+   "lam_trans". Minor INCOMPATIBILITY.
+ - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans".
+   Minor INCOMPATIBILITY.
+ - Added "opaque_combs" to option "lam_trans": lambda expressions are rewritten
+   using combinators, but the combinators are kept opaque, i.e. without
+   definitions.
+
+* Metis:
+ - Renamed option "hide_lams" to "opaque_lifting". Minor INCOMPATIBILITY.
 
 *** ML ***
 
diff -r fa92bc604c59 -r 269b2f976100 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jul 08 08:44:18 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jul 08 15:10:52 2021 +0200
@@ -975,14 +975,15 @@
 translation schemes are listed below:
 
 \begin{enum}
-\item[\labelitemi] \textbf{\textit{opaque\_lifting}:} Hide the
-$\lambda$-abstractions by replacing them by unspecified fresh constants,
-effectively disabling all reasoning under $\lambda$-abstractions.
-
 \item[\labelitemi] \textbf{\textit{lifting}:} Introduce a new
 supercombinator \const{c} for each cluster of $n$~$\lambda$-abstractions,
 defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
 
+\item[\labelitemi] \textbf{\textit{opaque\_lifting}:} Same as
+\textbf{\textit{lifting}}, except that the supercombinators are kept opaque,
+i.e. they are unspecified fresh constants. This effectively disables all
+reasoning under $\lambda$-abstractions.
+
 \item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
 combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
 enable the ATPs to synthesize $\lambda$-terms but tend to yield bulkier formulas
@@ -990,6 +991,10 @@
 equational definitions of the combinators are very prolific in the context of
 resolution.
 
+\item[\labelitemi] \textbf{\textit{opaque\_combs}:} Same as
+\textbf{\textit{combs}}, except that the combinators are kept opaque,
+i.e. without equational definitions.
+
 \item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new
 supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
 lifted equation $\const{c}~x_1~\ldots~x_n = t$ and via Curry combinators.