From 4b2d808b3297a307395d19fcf1502b4687e9120d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Oct 2006 15:58:50 +0000 Subject: [PATCH] Syntax of paramodulation parameters changed. --- helm/software/components/tactics/declarative.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index 4dcf38b6d..c7e5579f8 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -130,7 +130,7 @@ let rewritingstep ~dbd lhs rhs just conclude = match just with None -> Tactics.auto ~dbd - ~params:["paramodulation","on"; "timeout","3"] + ~params:["paramodulation","1"; "timeout","3"] | Some just -> Tactics.apply just in match lhs with -- 2.39.5