# HG changeset patch
# User wenzelm
# Date 1710970338 -3600
#      Wed Mar 20 22:32:18 2024 +0100
# Node ID 6f574c87ab99f0fe09080536c4f36f0ba7eb81fa
# Parent  f51730d25fc3e688e4e3ec5ae0dd96f0f555d068
test

diff -r f51730d25fc3 -r 6f574c87ab99 thys/Given_Clause_Loops/DISCOUNT_Loop.thy
--- a/thys/Given_Clause_Loops/DISCOUNT_Loop.thy	Tue Mar 19 16:45:23 2024 +0100
+++ b/thys/Given_Clause_Loops/DISCOUNT_Loop.thy	Wed Mar 20 22:32:18 2024 +0100
@@ -314,7 +314,7 @@
   then have "(T, labeled_formulas_of (P, {}, A) \<union> {(C, YY)}) \<leadsto>LGC
     (T \<union> T', labeled_formulas_of (P, {}, A) \<union> {(C, Active)})"
     using lgc.step.schedule_infer by blast
-  then show ?thesis
+  then show ?thesis sledgehammer [cvc5, mepo, slices = 2]
     by (metis state.simps P0A_add_y_formula PYA_add_active_formula)
 qed