move Taclet options of WD from key.core to key.core.wd

key.core.wd/src/main/resources/de/uka/ilkd/key/proof/rules/wdHeader.key

@@ -2,6 +2,51 @@
  * KeY is licensed under the GNU General Public License Version 2
  * SPDX-License-Identifier: GPL-2.0-only */
 
+\optionsDecl {
+		/*!
+    Treatment of formulas and terms for welldefinedness checks:
+    */
+    wdOperator: {
+        /*!
+        More intuitive for software developers and along the lines of
+        runtime assertion semantics. Well-Definedness checks will be
+        stricter using this operator, since the order of terms/formulas
+        matters. It is based on McCarthy logic.
+        Cf. "Are the Logical Foundations of Verifying Compiler
+        Prototypes Matching User Expectations?" by Patrice Chalin.
+
+        @choiceDefaultOption
+        */
+        L,
+        /*!
+        Complete and along the lines of classical logic, where the
+        order of terms/formulas is irrelevant. This operator is
+        equivalent to the D-operator, but more efficient.
+        Cf. "Efficient Well-Definedness Checking" by Ádám Darvas,
+        Farhad Mehta, and Arsenii Rudich.
+        */
+        Y,
+        /*!
+        Complete and along the lines of classical logic, where the
+        order of terms/formulas is irrelevant. This operator is not as
+        strict as the L-operator, based on strong Kleene logic. To be
+        used with care, since formulas may blow up exponentially.
+        Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and
+        Jean-Marc Meynadier*/
+        D
+    };
+
+    /*!
+    Welldefinedness checks of JML specifications can be turned on/off.
+    This includes class invariants, operation contracts, model fields
+    as well as JML (annotation) statements as loop invariants and
+    block contracts. The former ones are checked "on-the-fly", i.e.,
+    directly when they are applied in the code while proving an operation
+    contract, since the context is needed.
+    */
+    wdChecks: {off, on};
+}
+
 \transformers {
     \formula wd(any);
     \formula WD(\formula);

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/optionsDeclarations.key

@@ -160,48 +160,7 @@
     integerSimplificationRules: {full, /*! @choiceIncomplete */ minimal}; // TODO: further refine this option
     permissions: {off, on};
 
-    /*!
-    Treatment of formulas and terms for welldefinedness checks:
-    */
-    wdOperator: {
-        /*!
-        More intuitive for software developers and along the lines of
-        runtime assertion semantics. Well-Definedness checks will be
-        stricter using this operator, since the order of terms/formulas
-        matters. It is based on McCarthy logic.
-        Cf. "Are the Logical Foundations of Verifying Compiler
-        Prototypes Matching User Expectations?" by Patrice Chalin.
-
-        @choiceDefaultOption
-        */
-        L,
-        /*!
-        Complete and along the lines of classical logic, where the
-        order of terms/formulas is irrelevant. This operator is
-        equivalent to the D-operator, but more efficient.
-        Cf. "Efficient Well-Definedness Checking" by Ádám Darvas,
-        Farhad Mehta, and Arsenii Rudich.
-        */
-        Y,
-        /*!
-        Complete and along the lines of classical logic, where the
-        order of terms/formulas is irrelevant. This operator is not as
-        strict as the L-operator, based on strong Kleene logic. To be
-        used with care, since formulas may blow up exponentially.
-        Cf. "Well Defined B" by Patrick Behm, Lilian Burdy, and
-        Jean-Marc Meynadier*/
-        D
-    };
 
-    /*!
-    Welldefinedness checks of JML specifications can be turned on/off.
-    This includes class invariants, operation contracts, model fields
-    as well as JML (annotation) statements as loop invariants and
-    block contracts. The former ones are checked "on-the-fly", i.e.,
-    directly when they are applied in the code while proving an operation
-    contract, since the context is needed.
-    */
-    wdChecks: {off, on};
     /*!
     Specifies whether a special goal "Joined node is weakening" should be
     generated as a child of the partner node of a join operation.