--- 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
--- 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 ***
--- 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.