--- a/src/HOL/Metis_Examples/Abstraction.thy Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Metis_Examples/Abstraction.thy Mon Jan 31 16:09:23 2022 +0100
@@ -8,14 +8,14 @@
section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close>
theory Abstraction
-imports "HOL-Library.FuncSet"
+ imports "HOL-Library.FuncSet"
begin
(* For Christoph Benzmüller *)
lemma "x < 1 \<and> ((=) = (=)) \<Longrightarrow> ((=) = (=)) \<and> x < (2::nat)"
by (metis nat_1_add_1 trans_less_add2)
-lemma "((=) ) = (\<lambda>x y. y = x)"
+lemma "(=) = (\<lambda>x y. y = x)"
by metis
consts
--- a/src/HOL/Metis_Examples/Proxies.thy Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Metis_Examples/Proxies.thy Mon Jan 31 16:09:23 2022 +0100
@@ -14,8 +14,8 @@
imports Type_Encodings
begin
-sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,
- dont_minimize]
+sledgehammer_params [prover = spass, fact_filter = mepo, slices = 1, timeout = 30,
+ preplay_timeout = 0, dont_minimize]
text \<open>Extensionality and set constants\<close>