diff --git a/docs/user_manual.md b/docs/user_manual.md
index bacd78ff2f8..cfb08129172 100644
--- a/docs/user_manual.md
+++ b/docs/user_manual.md
@@ -360,7 +360,7 @@ string, which serves as a unique internal identifier and also is used in kast
 format of that syntax. If we need to reference a certain syntax production
 externally, we have to manually define the klabels using the `klabel` attribute.
 One example of where you would want to do this is to be able to refer to a given
-symbol via the `syntax priorities` attribute, or to enable overloading of a
+symbol via the `syntax priority` attribute, or to enable overloading of a
 given symbol.
 
 If you only provide the `klabel` attribute, you can use the provided `klabel` to
@@ -810,7 +810,7 @@ modularity. As a result, it becomes infeasible to declare priority and
 associativity inline within a set of productions, because the productions
 are not contiguous within a single file.
 
-For this purpose, we introduce the equivalent `syntax priorities`,
+For this purpose, we introduce the equivalent `syntax priority`,
 `syntax left`, `syntax right`, and `syntax non-assoc` declarations. For
 example, the above grammar can be written equivalently as:
 
@@ -820,7 +820,7 @@ syntax Exp ::= Exp "*" Exp [group(mult)]
              | Exp "+" Exp [group(add)]
              | Exp "-" Exp [group(sub)]
 
-syntax priorities mult div > add sub
+syntax priority mult div > add sub
 syntax left mult div
 syntax right add sub
 ```
@@ -836,7 +836,7 @@ syntax Exp ::= Exp "*" Exp [group(mult)]
              | Exp "+" Exp [group(add)]
              | Exp "-" Exp [group(add)]
 
-syntax priorities mult > add
+syntax priority mult > add
 syntax left mult
 syntax right add
 ```
@@ -844,7 +844,7 @@ syntax right add
 Note that `syntax [left|right|non-assoc]` should not be used to group together
 productions with different priorities. For example, this code would be invalid:
 ```k
-syntax priorities mult > add
+syntax priority mult > add
 syntax left mult add
 ```
 
diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md
index 1fe76acad64..be2702e2f5c 100644
--- a/k-distribution/include/kframework/builtin/domains.md
+++ b/k-distribution/include/kframework/builtin/domains.md
@@ -17,7 +17,7 @@ function on an undefined input, the behavior is undefined. In particular, when
 this happens, interpreters generated by the K LLVM backend may crash.
 
 ```k
-require "kast.md"
+requires "kast.md"
 ```
 
 Default Modules
@@ -256,7 +256,7 @@ left and the value is on the right.
 ```k
   syntax Map ::= KItem "|->" KItem                      [function, total, hook(MAP.element), klabel(_|->_), symbol, injective]
 
-  syntax priorities _|->_ > _Map_ .Map
+  syntax priority _|->_ > _Map_ .Map
   syntax non-assoc _|->_
 ```
 
@@ -524,7 +524,7 @@ of keys is on the left, and the value is on the right.
 ```k
   syntax RangeMap ::= Range "r|->" KItem                      [function, hook(RANGEMAP.elementRng), klabel(_r|->_), symbol, injective]
 
-  syntax priorities _r|->_ > _RangeMap_ .RangeMap
+  syntax priority _r|->_ > _RangeMap_ .RangeMap
   syntax non-assoc _r|->_
 ```
 
@@ -2277,15 +2277,15 @@ module K-EQUAL-SYNTAX
                   K "==K" K           [function, total, comm, smt-hook(=), hook(KEQUAL.eq), klabel(_==K_), symbol, group(equalEqualK)]
                 | K "=/=K" K          [function, total, comm, smt-hook(distinct), hook(KEQUAL.ne), klabel(_=/=K_), symbol, group(notEqualEqualK)]
 
-  syntax priorities equalEqualK notEqualEqualK > boolOperation mlOp
+  syntax priority equalEqualK notEqualEqualK > boolOperation mlOp
 
   syntax {Sort} Sort ::= "#if" Bool "#then" Sort "#else" Sort "#fi" [function, total, symbol(ite), smt-hook(ite), hook(KEQUAL.ite)]
 
 endmodule
 
 module K-EQUAL-KORE [symbolic]
-  import private BOOL
-  import K-EQUAL-SYNTAX
+  imports private BOOL
+  imports K-EQUAL-SYNTAX
 
   rule K1:Bool ==K K2:Bool => K1 ==Bool K2 [simplification]
   rule {K1 ==K K2 #Equals true} => {K1 #Equals K2} [simplification]
@@ -2300,9 +2300,9 @@ module K-EQUAL-KORE [symbolic]
 endmodule
 
 module K-EQUAL
-  import private BOOL
-  import K-EQUAL-SYNTAX
-  import K-EQUAL-KORE
+  imports private BOOL
+  imports K-EQUAL-SYNTAX
+  imports K-EQUAL-KORE
 
   rule K1:K =/=K K2:K => notBool (K1 ==K K2)
 
diff --git a/k-distribution/include/kframework/builtin/ffi.md b/k-distribution/include/kframework/builtin/ffi.md
index 812b47eb03c..3bba4fdd94e 100644
--- a/k-distribution/include/kframework/builtin/ffi.md
+++ b/k-distribution/include/kframework/builtin/ffi.md
@@ -18,7 +18,7 @@ to memory corruption in your interpreter and can cause segmentation faults or
 corrupted term representations that lead to undefined behavior at runtime.
 
 ```k
-require "domains.md"
+requires "domains.md"
 
 module FFI-SYNTAX
   imports private LIST
diff --git a/k-distribution/include/kframework/builtin/kast.md b/k-distribution/include/kframework/builtin/kast.md
index db3957151c9..1db02b34144 100644
--- a/k-distribution/include/kframework/builtin/kast.md
+++ b/k-distribution/include/kframework/builtin/kast.md
@@ -144,13 +144,13 @@ module ML-SYNTAX [not-lr1]
                                 | "#Floor" "(" Sort1 ")" [klabel(#Floor), symbol, mlOp, group(mlUnary, mlOp)]
                                 | "{" Sort1 "#Equals" Sort1 "}" [klabel(#Equals), symbol, mlOp, group(mlEquals, mlOp), comm, format(%1%i%n%2%d%n%3%i%n%4%d%n%5)]
 
-  syntax priorities mlUnary > mlEquals > mlAnd
+  syntax priority mlUnary > mlEquals > mlAnd
 
   syntax {Sort} Sort ::= Sort "#And" Sort [klabel(#And), symbol, assoc, left, comm, unit(#Top), mlOp, group(mlAnd, mlOp), format(%i%1%d%n%2%n%i%3%d)]
                        > Sort "#Or" Sort [klabel(#Or), symbol, assoc, left, comm, unit(#Bottom), mlOp, group(mlOp), format(%i%1%d%n%2%n%i%3%d)]
                        > Sort "#Implies" Sort [klabel(#Implies), symbol, mlOp, group(mlImplies, mlOp), format(%i%1%d%n%2%n%i%3%d)]
 
-  syntax priorities mlImplies > mlQuantifier
+  syntax priority mlImplies > mlQuantifier
 
   syntax {Sort1, Sort2} Sort2 ::= "#Exists" Sort1 "." Sort2 [klabel(#Exists), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)]
                                 | "#Forall" Sort1 "." Sort2 [klabel(#Forall), symbol, mlOp, mlBinder, group(mlQuantifier, mlOp)]
diff --git a/k-distribution/include/kframework/builtin/prelude.md b/k-distribution/include/kframework/builtin/prelude.md
index 14e426e57c9..92f850128dc 100644
--- a/k-distribution/include/kframework/builtin/prelude.md
+++ b/k-distribution/include/kframework/builtin/prelude.md
@@ -16,6 +16,6 @@ with `kompile -E`, or if you wish to modify the inner syntax of K by providing
 your own version of these files with different syntax.
 
 ```k
-require "kast.md"
-require "domains.md"
+requires "kast.md"
+requires "domains.md"
 ```
diff --git a/k-distribution/include/kframework/builtin/unification.k b/k-distribution/include/kframework/builtin/unification.k
index e359e080128..2efbef13a27 100644
--- a/k-distribution/include/kframework/builtin/unification.k
+++ b/k-distribution/include/kframework/builtin/unification.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "domains.md"
+requires "domains.md"
 module UNIFICATION
   imports SET
 
diff --git a/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md b/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md
index a50bfea8040..59c05ee2954 100644
--- a/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md
+++ b/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md
@@ -207,7 +207,7 @@ module LESSON-04-D
                    | Boolean "^" Boolean [group(xor), function]
                    | Boolean "||" Boolean [group(or), function]
 
-  syntax priorities literal atom > not > and > xor > or
+  syntax priority literal atom > not > and > xor > or
   syntax left and
   syntax left xor
   syntax left or
@@ -216,13 +216,13 @@ endmodule
 
 This introduces a couple of new features of K. First, the `group(_)` attribute
 is used to conceptually group together sets of sentences under a common
-user-defined name. For example, `literal` in the `syntax priorities` sentence is
+user-defined name. For example, `literal` in the `syntax priority` sentence is
 used to refer to all the productions marked with the `group(literal)` attribute,
 i.e., `true` and `false`. A production can belong to multiple groups using
 syntax such as `group(myGrp1,myGrp2)`.
 
 Once we understand this, it becomes relatively straightforward to understand
-the meaning of this grammar. Each `syntax priorities` sentence defines a
+the meaning of this grammar. Each `syntax priority` sentence defines a
 priority relation where `>` separates different priority groups. Each priority
 group is defined by a list of one or more group names, and consists of all
 productions which are members of at least one of those named groups.
diff --git a/k-distribution/src/test/resources/compiler-tests/assoc-test.k b/k-distribution/src/test/resources/compiler-tests/assoc-test.k
index baa83f4f4e2..c706635c5a5 100644
--- a/k-distribution/src/test/resources/compiler-tests/assoc-test.k
+++ b/k-distribution/src/test/resources/compiler-tests/assoc-test.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "domains.md"
+requires "domains.md"
 
 module ASSOC-TEST
   imports INT
diff --git a/k-distribution/src/test/resources/convertor-tests/configuration-kilexpected.k b/k-distribution/src/test/resources/convertor-tests/configuration-kilexpected.k
index 0e1edb52f48..eb5bae76817 100644
--- a/k-distribution/src/test/resources/convertor-tests/configuration-kilexpected.k
+++ b/k-distribution/src/test/resources/convertor-tests/configuration-kilexpected.k
@@ -1,7 +1,7 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
 DEF: null -> null
-require "include.k"
+requires "include.k"
 module INCLUDE
   syntax #Bool ::= "false"
 
diff --git a/k-distribution/src/test/resources/convertor-tests/configuration.k b/k-distribution/src/test/resources/convertor-tests/configuration.k
index 02bc584b4e2..eb05e8aad56 100644
--- a/k-distribution/src/test/resources/convertor-tests/configuration.k
+++ b/k-distribution/src/test/resources/convertor-tests/configuration.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "include.k"
+requires "include.k"
 
 module TEST
   imports INCLUDE
diff --git a/k-distribution/src/test/resources/convertor-tests/context.k b/k-distribution/src/test/resources/convertor-tests/context.k
index 23d602b3991..a98597d7d58 100644
--- a/k-distribution/src/test/resources/convertor-tests/context.k
+++ b/k-distribution/src/test/resources/convertor-tests/context.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "include.k"
+requires "include.k"
 
 module TEST
   imports INCLUDE
diff --git a/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k b/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k
index 18d81483e79..5a5f57cc66b 100644
--- a/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k
+++ b/k-distribution/src/test/resources/convertor-tests/imp_lesson1.k
@@ -1,10 +1,10 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module IMP-SYNTAX
-  import ID
-  import INT
-  import BOOL
+  imports ID
+  imports INT
+  imports BOOL
 
   syntax AExp  ::= Int | Id
                  | AExp "/" AExp              [left, strict]
diff --git a/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k b/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k
index e1ca6e67358..06598fa1789 100644
--- a/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k
+++ b/k-distribution/src/test/resources/convertor-tests/imp_lesson2.k
@@ -1,10 +1,10 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module IMP-SYNTAX
-  import ID
-  import INT
-  import BOOL
+  imports ID
+  imports INT
+  imports BOOL
 
   syntax AExp  ::= Int | Id
                  | AExp "/" AExp              [left, strict]
@@ -30,7 +30,7 @@ endmodule
 
 module IMP
   imports IMP-SYNTAX
-  import MAP
+  imports MAP
   syntax KResult ::= Int | Bool
 
   configuration <T color="yellow">
diff --git a/k-distribution/src/test/resources/convertor-tests/kore_varlabel.k b/k-distribution/src/test/resources/convertor-tests/kore_varlabel.k
index e614aaa1053..24f661598f5 100644
--- a/k-distribution/src/test/resources/convertor-tests/kore_varlabel.k
+++ b/k-distribution/src/test/resources/convertor-tests/kore_varlabel.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "domains.md"
+requires "domains.md"
 
 module VARLABEL-SYNTAX
 
diff --git a/k-distribution/src/test/resources/convertor-tests/simpleNestedConfiguration.k b/k-distribution/src/test/resources/convertor-tests/simpleNestedConfiguration.k
index 769c01cc722..e8a2ffbc18a 100644
--- a/k-distribution/src/test/resources/convertor-tests/simpleNestedConfiguration.k
+++ b/k-distribution/src/test/resources/convertor-tests/simpleNestedConfiguration.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module FUNC
     syntax Foo ::= "foo"
diff --git a/k-distribution/src/test/resources/convertor-tests/simpleNestedFunctions.k b/k-distribution/src/test/resources/convertor-tests/simpleNestedFunctions.k
index 2feba1b0edc..f795fb100d0 100644
--- a/k-distribution/src/test/resources/convertor-tests/simpleNestedFunctions.k
+++ b/k-distribution/src/test/resources/convertor-tests/simpleNestedFunctions.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "misc.k"
+requires "misc.k"
 
 module FUNC
     syntax Foo ::= "foo" Bar    [klabel(foo), function]
diff --git a/k-distribution/src/test/resources/convertor-tests/syntaxPriorities-kilexpected.k b/k-distribution/src/test/resources/convertor-tests/syntaxPriorities-kilexpected.k
index 87df320c8c6..91274fb2f57 100644
--- a/k-distribution/src/test/resources/convertor-tests/syntaxPriorities-kilexpected.k
+++ b/k-distribution/src/test/resources/convertor-tests/syntaxPriorities-kilexpected.k
@@ -15,7 +15,7 @@ module TEST
 
   syntax left t m
 
-  syntax prioritiesx
+  syntax priorityx
 > y z
 > t m
 > u
diff --git a/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities-kilexpected.k b/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities-kilexpected.k
index ca3c7e032f8..03389d69d1d 100644
--- a/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities-kilexpected.k
+++ b/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities-kilexpected.k
@@ -13,7 +13,7 @@ module TEST
 
   syntax left x
 
-  syntax prioritiesx
+  syntax priorityx
 > y z
 > t
 > u
diff --git a/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities.k b/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities.k
index 13959dd3d8f..d7304447e43 100644
--- a/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities.k
+++ b/k-distribution/src/test/resources/convertor-tests/syntaxWithPriorities.k
@@ -7,7 +7,7 @@ module TEST
                | "t"    [andanohter]
                | "u"    [off]
 
-  syntax priorities x > y z > t > u
+  syntax priority x > y z > t > u
   syntax left x
   syntax right y
 endmodule
diff --git a/k-distribution/tests/profiling/elrond-semantics/test.k b/k-distribution/tests/profiling/elrond-semantics/test.k
index 5e72bdf7b4c..852c902f741 100644
--- a/k-distribution/tests/profiling/elrond-semantics/test.k
+++ b/k-distribution/tests/profiling/elrond-semantics/test.k
@@ -2188,7 +2188,7 @@ module MAP-BYTES-TO-BYTES
     ".MapBytesToBytes" [function, hook(MAP.unit), klabel(.MapBytesToBytes), symbol, total]
   syntax MapBytesToBytes  ::=
     WrappedBytes "Bytes2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Bytes2Bytes|->_), symbol, total]
-  syntax priorities _Bytes2Bytes|->_  > _MapBytesToBytes_ .MapBytesToBytes
+  syntax priority _Bytes2Bytes|->_  > _MapBytesToBytes_ .MapBytesToBytes
   syntax non-assoc _Bytes2Bytes|->_
   syntax WrappedBytes  ::=
     MapBytesToBytes "[" WrappedBytes "]" [function, hook(MAP.lookup), klabel(MapBytesToBytes:lookup), symbol]
@@ -2570,7 +2570,7 @@ module MAP-INT-TO-BYTES
     ".MapIntToBytes" [function, hook(MAP.unit), klabel(.MapIntToBytes), symbol, total]
   syntax MapIntToBytes  ::=
     WrappedInt "Int2Bytes|->" WrappedBytes [function, hook(MAP.element), injective, klabel(_Int2Bytes|->_), symbol, total]
-  syntax priorities _Int2Bytes|->_  > _MapIntToBytes_ .MapIntToBytes
+  syntax priority _Int2Bytes|->_  > _MapIntToBytes_ .MapIntToBytes
   syntax non-assoc _Int2Bytes|->_
   syntax WrappedBytes  ::=
     MapIntToBytes "[" WrappedInt "]" [function, hook(MAP.lookup), klabel(MapIntToBytes:lookup), symbol]
diff --git a/k-distribution/tests/regression-new/append/test.k b/k-distribution/tests/regression-new/append/test.k
index 3df9a6b66a0..71638b2fe4a 100644
--- a/k-distribution/tests/regression-new/append/test.k
+++ b/k-distribution/tests/regression-new/append/test.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEAL-SYNTAX
-  import INT-SYNTAX
+  imports INT-SYNTAX
 endmodule
 
 module TEST-SYNTAX
diff --git a/k-distribution/tests/regression-new/bracket-priority/test.k b/k-distribution/tests/regression-new/bracket-priority/test.k
index 2abf8957965..eb957a43d8d 100644
--- a/k-distribution/tests/regression-new/bracket-priority/test.k
+++ b/k-distribution/tests/regression-new/bracket-priority/test.k
@@ -13,6 +13,6 @@ syntax BuiltinName ::= "+"
 
 rule (+ I1:Int I2:Int) => I1 +Int I2
 
-syntax priorities defaultBracket > expList
+syntax priority defaultBracket > expList
 
 endmodule
diff --git a/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k b/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k
index 00a04e11d69..ddde73b4366 100644
--- a/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k
+++ b/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "ffi.k"
+requires "ffi.k"
 
 module REQUIREBUILTINK-SYNTAX
 endmodule
diff --git a/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k.out b/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k.out
index dcb6d885522..bbf8c2bff34 100644
--- a/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k.out
+++ b/k-distribution/tests/regression-new/checkWarns/requireBuiltinK.k.out
@@ -1,5 +1,5 @@
 [Error] Compiler: Requiring a K file in the K builtin directory via a deprecated filename. Please replace "ffi.k" with "ffi.md".
 	Source(requireBuiltinK.k)
-	Location(2,1,2,16)
-	2 |	require "ffi.k"
-	  .	^~~~~~~~~~~~~~~
+	Location(2,1,2,17)
+	2 |	requires "ffi.k"
+	  .	^~~~~~~~~~~~~~~~
diff --git a/k-distribution/tests/regression-new/checks/binder.k b/k-distribution/tests/regression-new/checks/binder.k
index 62c12a285bb..9ce0d39f714 100644
--- a/k-distribution/tests/regression-new/checks/binder.k
+++ b/k-distribution/tests/regression-new/checks/binder.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "substitution.md"
+requires "substitution.md"
 
 module BINDER
   imports KVAR
diff --git a/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k b/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k
index ecb174c9cea..f3566aed947 100644
--- a/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k
+++ b/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k
@@ -1,4 +1,4 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEST
-  syntax priorities a > b
+  syntax priority a > b
 endmodule
diff --git a/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k.out b/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k.out
index ccc58568d30..eac478430ca 100644
--- a/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k.out
+++ b/k-distribution/tests/regression-new/checks/checkUndeclaredTags.k.out
@@ -1,5 +1,5 @@
 [Error] Outer Parser: Could not find any productions for tag: a
 	Source(checkUndeclaredTags.k)
-	Location(3,3,3,26)
-	3 |	  syntax priorities a > b
-	  .	  ^~~~~~~~~~~~~~~~~~~~~~~
+	Location(3,3,3,24)
+	3 |	  syntax priority a > b
+	  .	  ^~~~~~~~~~~~~~~~~~~~~
diff --git a/k-distribution/tests/regression-new/checks/missingKResult.k b/k-distribution/tests/regression-new/checks/missingKResult.k
index 16f8ed37887..ba73b06875a 100644
--- a/k-distribution/tests/regression-new/checks/missingKResult.k
+++ b/k-distribution/tests/regression-new/checks/missingKResult.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "substitution.md"
+requires "substitution.md"
 
 module MISSINGKRESULT
   imports DOMAINS
diff --git a/k-distribution/tests/regression-new/domains-lemmas-no-smt/domains-lemmas-no-smt.k b/k-distribution/tests/regression-new/domains-lemmas-no-smt/domains-lemmas-no-smt.k
index fdb46b01228..e2388a3849b 100644
--- a/k-distribution/tests/regression-new/domains-lemmas-no-smt/domains-lemmas-no-smt.k
+++ b/k-distribution/tests/regression-new/domains-lemmas-no-smt/domains-lemmas-no-smt.k
@@ -2,7 +2,7 @@
 requires "domains.md"
 
 module DOMAINS-LEMMAS-NO-SMT
-    import INT
+    imports INT
 
     configuration <k> $PGM:Pgm </k>
 
diff --git a/k-distribution/tests/regression-new/issue-1186/test.k b/k-distribution/tests/regression-new/issue-1186/test.k
index cef53a68312..b02e4c7749d 100644
--- a/k-distribution/tests/regression-new/issue-1186/test.k
+++ b/k-distribution/tests/regression-new/issue-1186/test.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "substitution.md"
+requires "substitution.md"
 
 module TEST
   imports KVAR
diff --git a/k-distribution/tests/regression-new/issue-1573/test.k b/k-distribution/tests/regression-new/issue-1573/test.k
index 345847a5a15..452031310d1 100644
--- a/k-distribution/tests/regression-new/issue-1573/test.k
+++ b/k-distribution/tests/regression-new/issue-1573/test.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEST
-  import INT
+  imports INT
 
   syntax IntList ::= List{Int, ""}
 
diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a1-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a1-spec.k
index 3380dfb8e8a..22ad3d8d133 100644
--- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a1-spec.k
+++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a1-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 
 
 module VERIFICATION
-  import TEST
+  imports TEST
 
   rule (X +Int Y) +Int Z => Z +Int (X +Int Y) [simplification, symbolic(X), concrete(Y, Z)]
   rule (X +Int Y) +Int Z => Y +Int (X +Int Z) [simplification, concrete(X, Z), symbolic(Y)]
@@ -13,7 +13,7 @@ module VERIFICATION
 endmodule
 
 module A1-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
   claim [s1]:
     <k> run(5) => .K </k> <counter> n => 0 </counter>
diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a2-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a2-spec.k
index fc4330bbf52..75a7d905305 100644
--- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a2-spec.k
+++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a2-spec.k
@@ -3,13 +3,13 @@ requires "test.k"
 
 
 module VERIFICATION
-  import TEST
+  imports TEST
 
   rule <k> (X +Int Y) +Int Z => Z +Int (X +Int Y) </k> [simplification, symbolic(X), concrete(Y, Z)]
 endmodule
 
 module A2-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
   claim [s1]:
     <k> run(5) => .K </k> <counter> n => 0 </counter>
diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a3-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a3-spec.k
index 0e129b20330..d0366c666e6 100644
--- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a3-spec.k
+++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a3-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 
 
 module A3-SPEC
-  import TEST
+  imports TEST
 
   rule [unif-map]: { MAP [ K <- V ] #Equals MAP:Map [ K <- V' ] } => { V #Equals V' } [simplification]
 
diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k
index 287a404999b..53d7088a269 100644
--- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k
+++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 // https://github.com/runtimeverification/k/issues/2587
 
 module A4-SPEC
-  import TEST
+  imports TEST
   imports ML-SYNTAX
 
   claim <k> c => 2 #And {3 #Equals n} </k>
diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k
index dc8b657977f..161080a8a05 100644
--- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k
+++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 // https://github.com/runtimeverification/k/issues/2587
 
 module A5-SPEC
-  import TEST
+  imports TEST
   imports ML-SYNTAX
 
   claim <k> c => 2 #And n +Int n </k>
diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a6-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a6-spec.k
index a7d52b395cf..7e088198b95 100644
--- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a6-spec.k
+++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a6-spec.k
@@ -3,13 +3,13 @@ requires "test.k"
 
 
 module VERIFICATION
-  import TEST
+  imports TEST
 
   rule notAFunction => 1 [simplification]
 endmodule
 
 module A6-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
   claim [s1]:
     <k> run(5) => .K </k> <counter> n => 0 </counter>
diff --git a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a1-spec.k b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a1-spec.k
index 5a19c5561e9..89cd472ce5b 100644
--- a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a1-spec.k
+++ b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a1-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 
 
 module VERIFICATION
-  import TEST
+  imports TEST
 
   rule (X +Int Y) +Int Z => Z +Int (X +Int Y) [simplification, symbolic(X), concrete(Y, Z)]
   rule (X +Int Y) +Int Z => Y +Int (X +Int Z) [simplification, concrete(X, Z), symbolic(Y)]
@@ -17,6 +17,6 @@ module VERIFICATION
 endmodule
 
 module A1-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
 endmodule
diff --git a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a2-spec.k b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a2-spec.k
index 181d7dfdedc..254dd000d1c 100644
--- a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a2-spec.k
+++ b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/claims/a2-spec.k
@@ -3,12 +3,12 @@ requires "test.k"
 
 
 module VERIFICATION
-  import TEST
+  imports TEST
   rule [s1]: notAFunction => 1 [simplification]
 
   claim <k> run(5) => .K </k> <counter> n => 0 </counter>
 endmodule
 
 module A2-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 endmodule
diff --git a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/exclude/a1-spec.k b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/exclude/a1-spec.k
index 383fe817cf8..a39c83d4ead 100644
--- a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/exclude/a1-spec.k
+++ b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/exclude/a1-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 
 
 module VERIFICATION
-  import TEST
+  imports TEST
 
   rule (X +Int Y) +Int Z => Z +Int (X +Int Y) [simplification, symbolic(X), concrete(Y, Z)]
   rule (X +Int Y) +Int Z => Y +Int (X +Int Z) [simplification, concrete(X, Z), symbolic(Y)]
@@ -19,6 +19,6 @@ module VERIFICATION
 endmodule
 
 module A1-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
 endmodule
diff --git a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/trusted/a1-spec.k b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/trusted/a1-spec.k
index 97581d6dbd3..34bb6b7d4a5 100644
--- a/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/trusted/a1-spec.k
+++ b/k-distribution/tests/regression-new/issue-2812-kprove-filter-claims/trusted/a1-spec.k
@@ -3,7 +3,7 @@ requires "test.k"
 
 
 module VERIFICATION
-  import TEST
+  imports TEST
 
   claim [s1]:
     <k> 1 => 2 </k> // should fail but marked as trusted whould pass
@@ -11,6 +11,6 @@ module VERIFICATION
 endmodule
 
 module A1-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
 endmodule
diff --git a/k-distribution/tests/regression-new/issue-3450-kprove-fresh/explicit-spec.k b/k-distribution/tests/regression-new/issue-3450-kprove-fresh/explicit-spec.k
index c72a120501a..ab545b16b6d 100644
--- a/k-distribution/tests/regression-new/issue-3450-kprove-fresh/explicit-spec.k
+++ b/k-distribution/tests/regression-new/issue-3450-kprove-fresh/explicit-spec.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "test.k"
+requires "test.k"
 
 module EXPLICIT-SPEC
     imports TEST
diff --git a/k-distribution/tests/regression-new/issue-3450-kprove-fresh/implicit-spec.k b/k-distribution/tests/regression-new/issue-3450-kprove-fresh/implicit-spec.k
index d5ea9a468a0..faa3ab4d4df 100644
--- a/k-distribution/tests/regression-new/issue-3450-kprove-fresh/implicit-spec.k
+++ b/k-distribution/tests/regression-new/issue-3450-kprove-fresh/implicit-spec.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "test.k"
+requires "test.k"
 
 module IMPLICIT-SPEC
     imports TEST
diff --git a/k-distribution/tests/regression-new/issue-3672-debugParse/test.k b/k-distribution/tests/regression-new/issue-3672-debugParse/test.k
index c6644735fe6..4df6720621a 100644
--- a/k-distribution/tests/regression-new/issue-3672-debugParse/test.k
+++ b/k-distribution/tests/regression-new/issue-3672-debugParse/test.k
@@ -12,7 +12,7 @@ module TEST-SYNTAX
                | Exp "/" Exp  [left, group(div)]
                | "(" Exp ")"  [bracket]
 
-  syntax priorities neg > mul div > add sub
+  syntax priority neg > mul div > add sub
 endmodule
 
 module TEST
diff --git a/k-distribution/tests/regression-new/itp/nth-ancestor/chain.k b/k-distribution/tests/regression-new/itp/nth-ancestor/chain.k
index 7238995eb1b..1c2a2c0c6e8 100644
--- a/k-distribution/tests/regression-new/itp/nth-ancestor/chain.k
+++ b/k-distribution/tests/regression-new/itp/nth-ancestor/chain.k
@@ -4,7 +4,7 @@
     https://github.com/runtimeverification/casper-proofs/blob/master/Core/AccountableSafety.v
 */
 
-require "proof-script.k"
+requires "proof-script.k"
 
 module CHAIN-SYNTAX
 
diff --git a/k-distribution/tests/regression-new/itp/nth-ancestor/verification.k b/k-distribution/tests/regression-new/itp/nth-ancestor/verification.k
index e4bbb961990..36cdab0140c 100644
--- a/k-distribution/tests/regression-new/itp/nth-ancestor/verification.k
+++ b/k-distribution/tests/regression-new/itp/nth-ancestor/verification.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "chain.k"
+requires "chain.k"
 
 module VERIFICATION-SYNTAX
 endmodule
diff --git a/k-distribution/tests/regression-new/kdep-options/remake-depend/a.k b/k-distribution/tests/regression-new/kdep-options/remake-depend/a.k
index 3a036949927..55db4b155f9 100644
--- a/k-distribution/tests/regression-new/kdep-options/remake-depend/a.k
+++ b/k-distribution/tests/regression-new/kdep-options/remake-depend/a.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "b.k"
+requires "b.k"
 
 module A
   imports B
diff --git a/k-distribution/tests/regression-new/kdep-options/simple/a.k b/k-distribution/tests/regression-new/kdep-options/simple/a.k
index d2f0f93ec07..8105c1e1cdb 100644
--- a/k-distribution/tests/regression-new/kdep-options/simple/a.k
+++ b/k-distribution/tests/regression-new/kdep-options/simple/a.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "b.k"
-require "c.k"
+requires "b.k"
+requires "c.k"
 
 module A
   imports B
diff --git a/k-distribution/tests/regression-new/kdep-options/simple/c.k b/k-distribution/tests/regression-new/kdep-options/simple/c.k
index 9a44319d932..568b5e84e0a 100644
--- a/k-distribution/tests/regression-new/kdep-options/simple/c.k
+++ b/k-distribution/tests/regression-new/kdep-options/simple/c.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "d.k"
+requires "d.k"
 
 module C
   imports D
diff --git a/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k b/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k
index cf84a4b7c54..53e7e5596c2 100644
--- a/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k
+++ b/k-distribution/tests/regression-new/kprove-error-status/stuck-claim-spec.k
@@ -4,7 +4,7 @@ module VERIFICATION
 endmodule
 
 module STUCK-CLAIM-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
   claim  <k> addCounter(N:Int) => 1 ...</k>
          <counter> C:Int => ?_ </counter>
diff --git a/k-distribution/tests/regression-new/kprove-haskell/sum-spec.k b/k-distribution/tests/regression-new/kprove-haskell/sum-spec.k
index a68123799bc..46a73cfe5a7 100644
--- a/k-distribution/tests/regression-new/kprove-haskell/sum-spec.k
+++ b/k-distribution/tests/regression-new/kprove-haskell/sum-spec.k
@@ -4,7 +4,7 @@ module VERIFICATION
 endmodule
 
 module SUM-SPEC
-  import VERIFICATION
+  imports VERIFICATION
 
   claim  <k> addCounter(N:Int) => .K ...</k>
          <counter> C:Int => ?_ </counter>
diff --git a/k-distribution/tests/regression-new/markdownSelectors/a-spec.md b/k-distribution/tests/regression-new/markdownSelectors/a-spec.md
index 9adb5083211..e352a0e4698 100644
--- a/k-distribution/tests/regression-new/markdownSelectors/a-spec.md
+++ b/k-distribution/tests/regression-new/markdownSelectors/a-spec.md
@@ -3,7 +3,7 @@ copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 ---
 
 ```k
-require "test.md"
+requires "test.md"
 
 module A-SPEC
 
diff --git a/k-distribution/tests/regression-new/parse-c/c18-syntax.k b/k-distribution/tests/regression-new/parse-c/c18-syntax.k
index a21b18be547..cd05dbacb33 100644
--- a/k-distribution/tests/regression-new/parse-c/c18-syntax.k
+++ b/k-distribution/tests/regression-new/parse-c/c18-syntax.k
@@ -97,8 +97,8 @@ module C18-COMMON
                | Exp "|=" Exp [group(assign)]
                > left:
                  Exp "," Exp [group(comma)]
-  syntax priorities assignExp > comma
-  syntax priorities constantExp > assign
+  syntax priority assignExp > comma
+  syntax priority constantExp > assign
 
   syntax GenericAssocs ::= NeList{GenericAssoc,","}
 
diff --git a/k-distribution/tests/regression-new/parse-c/c18-translation.k b/k-distribution/tests/regression-new/parse-c/c18-translation.k
index 553be454045..2bec3d05aae 100644
--- a/k-distribution/tests/regression-new/parse-c/c18-translation.k
+++ b/k-distribution/tests/regression-new/parse-c/c18-translation.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "c18-syntax.k"
+requires "c18-syntax.k"
 
 module C18-TRANSLATION-SYNTAX
   imports C18-SYNTAX
diff --git a/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k b/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k
index 15aa12449e0..c78b92a7b37 100644
--- a/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k
+++ b/k-distribution/tests/regression-new/pl-tutorial/1_k/1_lambda/lesson_8/lambda.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
+requires "substitution.md"
 
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
diff --git a/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md b/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
index 77eb77067b8..db442366b66 100644
--- a/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
+++ b/k-distribution/tests/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
@@ -363,16 +363,16 @@ a constructor for function types:
 ## Additional Priorities
 
 ```k
-  syntax priorities @__FUN-UNTYPED-COMMON
-                  > apply
-                  > arith
-                  > _:=__FUN-UNTYPED-COMMON
-                  > let_in__FUN-UNTYPED-COMMON
-                    letrec_in__FUN-UNTYPED-COMMON
-                    if_then_else__FUN-UNTYPED-COMMON
-                  > _;__FUN-UNTYPED-COMMON
-                  > fun__FUN-UNTYPED-COMMON
-                  > datatype_=___FUN-UNTYPED-COMMON
+  syntax priority @__FUN-UNTYPED-COMMON
+                > apply
+                > arith
+                > _:=__FUN-UNTYPED-COMMON
+                > let_in__FUN-UNTYPED-COMMON
+                  letrec_in__FUN-UNTYPED-COMMON
+                  if_then_else__FUN-UNTYPED-COMMON
+                > _;__FUN-UNTYPED-COMMON
+                > fun__FUN-UNTYPED-COMMON
+                > datatype_=___FUN-UNTYPED-COMMON
 endmodule
 
 module FUN-UNTYPED-MACROS
diff --git a/k-distribution/tests/regression-new/prelude-warnings/test.k b/k-distribution/tests/regression-new/prelude-warnings/test.k
index 7a67d862a53..367c593424f 100644
--- a/k-distribution/tests/regression-new/prelude-warnings/test.k
+++ b/k-distribution/tests/regression-new/prelude-warnings/test.k
@@ -1,8 +1,8 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "ffi.md"
-require "json.md"
-require "rat.md"
-require "substitution.md"
+requires "ffi.md"
+requires "json.md"
+requires "rat.md"
+requires "substitution.md"
 
 module TEST-SYNTAX
 endmodule
diff --git a/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-spec.k b/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-spec.k
index 28889364322..48a19c51dc9 100644
--- a/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-spec.k
+++ b/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "deposit-symbolic.k"
+requires "deposit-symbolic.k"
 
 module DEPOSIT-SPEC
 
diff --git a/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-symbolic.k b/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-symbolic.k
index 5fb96cc6a9b..209764c6619 100644
--- a/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-symbolic.k
+++ b/k-distribution/tests/regression-new/proof-tests/deposit/spec/deposit-symbolic.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "../test/deposit.k"
+requires "../test/deposit.k"
 
 module DEPOSIT-SYMBOLIC
 
diff --git a/k-distribution/tests/regression-new/proof-tests/deposit/test/deposit.k b/k-distribution/tests/regression-new/proof-tests/deposit/test/deposit.k
index 514044bbca1..dad99b553c9 100644
--- a/k-distribution/tests/regression-new/proof-tests/deposit/test/deposit.k
+++ b/k-distribution/tests/regression-new/proof-tests/deposit/test/deposit.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "imap.k"
+requires "imap.k"
 
 module DEPOSIT-SYNTAX
 
diff --git a/k-distribution/tests/regression-new/quadratic-poly-unparsing/nondet.k b/k-distribution/tests/regression-new/quadratic-poly-unparsing/nondet.k
index b09980786df..4460deb1f1f 100644
--- a/k-distribution/tests/regression-new/quadratic-poly-unparsing/nondet.k
+++ b/k-distribution/tests/regression-new/quadratic-poly-unparsing/nondet.k
@@ -1,7 +1,7 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module NONDET
 
-  import DOMAINS
+  imports DOMAINS
 
   syntax S
     ::= "initial"
diff --git a/k-distribution/tests/regression-new/simp-haskell/a.k b/k-distribution/tests/regression-new/simp-haskell/a.k
index d349dc7d0e8..1a762aa7248 100644
--- a/k-distribution/tests/regression-new/simp-haskell/a.k
+++ b/k-distribution/tests/regression-new/simp-haskell/a.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module A
-  import INT
+  imports INT
   syntax Int ::= abs(Int) [function, total]
                | "error" [function, total]
   rule abs(X:Int) => X:Int requires X >Int 0
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def01-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def01-spec.k
index 484af92f83c..aaf450c06b2 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def01-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def01-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // inc(Y) in pattern LHS. Function with no side conditions.
 module DEF01-SPEC
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def02-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def02-spec.k
index 31191b96fc4..1390acd4243 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def02-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def02-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // `requires Z ==Int incPos(Y)` - Function in requires, used in RHS. Does not affect matching.
 module DEF02-SPEC
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def031-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def031-spec.k
index b01fdd3921e..44b9b757db4 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def031-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def031-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X = Y,   `mid Y => end incPos(Y)` - Function in pattern RHS.
 module DEF031-SPEC
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def032-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def032-spec.k
index f78e7196918..6465e7f2d76 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def032-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def032-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X = Y-1, `mid Y => end incPos(Y)` - Function in pattern RHS.
 module DEF032-SPEC
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def033-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def033-spec.k
index db3e0ecddc8..a6fb4ae76e7 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def033-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def033-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X+1 = Y, `mid Y => end incPos(Y)` - Function in pattern RHS.
 module DEF033-SPEC
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def11-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def11-spec.k
index 0afe15a9eec..2bc0f70541a 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def11-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def11-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y (in pattern) matching.
 // inc(Y) in pattern LHS. Function with no side conditions. Evaluation required for planned matching.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def12-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def12-spec.k
index 389d5cf5114..f9f6f197fdb 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def12-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def12-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y (in pattern) matching.
 // `requires Z ==Int incPos(Y)` - Function in requires, used in another cell in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def13-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def13-spec.k
index 7e52c217ec9..5375cceb265 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def13-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def13-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y (in pattern) matching.
 // `requires Y ==Int incPos(Y) -Int 1` - Function in requires, used in LHS, same var as one matched in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def14-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def14-spec.k
index 1f9a2ec33da..240defee176 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def14-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def14-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y (in pattern) matching.
 // `<var> incPos(Y) +Int 1 </var>` - Function directly in another cell in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def15-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def15-spec.k
index 0eeaf1248f1..359bba3f98c 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def15-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def15-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y (in pattern) matching.
 // `requires incPos(Y) ==Int Y +Int 1` - Function in requires that is not substitution.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def21-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def21-spec.k
index 7e9f2542691..0a20933613f 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def21-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def21-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X+1 (in term) = Y (in pattern) matching.
 // inc(Y) in pattern LHS. Function with no side conditions. Evaluation required for planned matching.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def22-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def22-spec.k
index dd2df04c49c..b2349f34729 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def22-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def22-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X+1 (in term) = Y (in pattern) matching.
 //`requires Z ==Int incPos(Y)` - Function in requires, used in another cell in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def23-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def23-spec.k
index 9ab0c19e18e..0542653ce95 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def23-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def23-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X+1 (in term) = Y (in pattern) matching.
 // `requires Y ==Int incPos(Y) -Int 1` - Function in requires, used in LHS, same var as one matched in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def24-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def24-spec.k
index f9ca2bbe01a..5d0b751f2cd 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def24-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def24-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X+1 (in term) = Y (in pattern) matching.
 // `<var> incPos(Y) +Int 1 </var>` - Function directly in another cell in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def25-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def25-spec.k
index 7f40a6bd707..be8ee95aca6 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def25-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def25-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X+1 (in term) = Y (in pattern) matching.
 // `requires incPos(Y) ==Int Y +Int 1` - Function in requires that is not substitution.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def41-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def41-spec.k
index 5c24de6f4c4..5dad6880cd6 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def41-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def41-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 /*
 Part 4. Substitutions of RHS vars must be preferred over LHS vars, for cases var = term
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def42-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def42-spec.k
index 4f4cfd427a9..24eaa280888 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def42-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def42-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 /*
 Part 4. Substitutions of RHS vars must be preferred over LHS vars, for cases var = term
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def44-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def44-spec.k
index 5f1c9eb77b9..4b36a4cf5e5 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def44-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def44-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // 2 equalities can generate mutually exclusive substitutions.
 // Situation similar to what is found in ERC2.0 high-level contract
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def45-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def45-spec.k
index a7ede54277a..6c1e12b4970 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def45-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def45-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // 2 equalities can generate mutually exclusive substitutions.
 // Situation similar to what is found in ERC2.0 high-level contract
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def61-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def61-spec.k
index 28ab76e89e8..345e7cc9a9b 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def61-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def61-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 /*
 Part 6. Term must be always simplified/evaluated under current constraint.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def62-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def62-spec.k
index ec96d820cc5..4b69a484d74 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def62-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def62-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 /*
 Part 6. Term must be always simplified/evaluated under current constraint.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def71-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def71-spec.k
index 5bc3b69d832..bf613d654e9 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def71-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def71-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 /*
 Part 7: Unification (with function evaluation) must be preferred over substitution, after each substituted var.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/def81-spec.k b/k-distribution/tests/regression-new/spec-rule-application/def81-spec.k
index 9283421e1a2..e6cb412ca6d 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/def81-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/def81-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 /*
 Part 8. Initial simplification must have access to pattern constraint (e.g. spec rule side condition),
diff --git a/k-distribution/tests/regression-new/spec-rule-application/fail/def32-spec.k b/k-distribution/tests/regression-new/spec-rule-application/fail/def32-spec.k
index 1f71d4eb60b..7ca490eb0c3 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/fail/def32-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/fail/def32-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y-1 (in pattern) matching.
 // `requires Z ==Int incPos(Y)` - Function in requires, used in another cell in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/fail/def33-spec.k b/k-distribution/tests/regression-new/spec-rule-application/fail/def33-spec.k
index 53a0f4d4c03..5c30c7dd656 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/fail/def33-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/fail/def33-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y-1 (in pattern) matching.
 // `requires Y ==Int incPos(Y) -Int 1` - Function in requires, used in LHS, same var as one matched in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/fail/def34-spec.k b/k-distribution/tests/regression-new/spec-rule-application/fail/def34-spec.k
index e8d9dec64dd..fdd9c0ab0ba 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/fail/def34-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/fail/def34-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y-1 (in pattern) matching.
 // `<var> incPos(Y) +Int 1 </var>` - Function directly in another cell in LHS.
diff --git a/k-distribution/tests/regression-new/spec-rule-application/fail/def35-spec.k b/k-distribution/tests/regression-new/spec-rule-application/fail/def35-spec.k
index db4bd9e2c9d..65f4b8be024 100644
--- a/k-distribution/tests/regression-new/spec-rule-application/fail/def35-spec.k
+++ b/k-distribution/tests/regression-new/spec-rule-application/fail/def35-spec.k
@@ -1,5 +1,5 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
-require "def.k"
+requires "def.k"
 
 // X (in term) = Y-1 (in pattern) matching.
 // `requires incPos(Y) ==Int Y +Int 1` - Function in requires that is not substitution.
diff --git a/k-distribution/tests/smoke/kparse-test/test.k b/k-distribution/tests/smoke/kparse-test/test.k
index 3df9a6b66a0..71638b2fe4a 100644
--- a/k-distribution/tests/smoke/kparse-test/test.k
+++ b/k-distribution/tests/smoke/kparse-test/test.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 module TEAL-SYNTAX
-  import INT-SYNTAX
+  imports INT-SYNTAX
 endmodule
 
 module TEST-SYNTAX
diff --git a/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java b/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java
index a7cee5bd5cc..88dc665b6cc 100644
--- a/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java
+++ b/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java
@@ -5,7 +5,7 @@
 import org.kframework.definition.Tag;
 
 /**
- * A group within a {@code syntax priorities} declaration.
+ * A group within a {@code syntax priority} declaration.
  *
  * @see PriorityExtended
  */
diff --git a/kernel/src/main/java/org/kframework/kil/PriorityExtended.java b/kernel/src/main/java/org/kframework/kil/PriorityExtended.java
index d273a2d9878..640deb17604 100644
--- a/kernel/src/main/java/org/kframework/kil/PriorityExtended.java
+++ b/kernel/src/main/java/org/kframework/kil/PriorityExtended.java
@@ -2,7 +2,7 @@
 package org.kframework.kil;
 
 /**
- * A priority declaration, {@code syntax priorities} <em>labels</em> {@code >} ... {@code >}
+ * A priority declaration, {@code syntax priority} <em>labels</em> {@code >} ... {@code >}
  * <em>labels</em>.
  *
  * @see PriorityBlockExtended
@@ -22,7 +22,7 @@ public java.util.List<PriorityBlockExtended> getPriorityBlocks() {
 
   @Override
   public void toString(StringBuilder sb) {
-    sb.append("  syntax priorities ");
+    sb.append("  syntax priority ");
     String conn = "";
     for (PriorityBlockExtended pb : priorityBlocks) {
       sb.append(conn);
diff --git a/kernel/src/main/java/org/kframework/kil/Require.java b/kernel/src/main/java/org/kframework/kil/Require.java
index c4dc6d54c66..b9ba502d4e1 100644
--- a/kernel/src/main/java/org/kframework/kil/Require.java
+++ b/kernel/src/main/java/org/kframework/kil/Require.java
@@ -5,7 +5,7 @@
 
 /** A require directive */
 public class Require extends DefinitionItem {
-  /** The string argument to {@code require}, as written in the input file. */
+  /** The string argument to {@code requires}, as written in the input file. */
   private String value;
 
   public Require(String value) {
@@ -23,7 +23,7 @@ public String getValue() {
 
   @Override
   public void toString(StringBuilder sb) {
-    sb.append("require ");
+    sb.append("requires ");
     sb.append(StringUtil.enquoteCString(value));
   }
 }
diff --git a/kernel/src/test/java/org/kframework/lsp/LSPTests.java b/kernel/src/test/java/org/kframework/lsp/LSPTests.java
index 65b6ec6a5fb..13f53b99492 100644
--- a/kernel/src/test/java/org/kframework/lsp/LSPTests.java
+++ b/kernel/src/test/java/org/kframework/lsp/LSPTests.java
@@ -31,8 +31,8 @@
 public class LSPTests {
 
   String def =
-      "//require \"Copy (10) test.k\"\n"
-          + "require \"spec.k\"\n"
+      "//requires \"Copy (10) test.k\"\n"
+          + "requires \"spec.k\"\n"
           + "\n"
           + "module A\n"
           + "  syntax A ::= \"a\"\n"
@@ -63,7 +63,7 @@ public class LSPTests {
   public void testGetContext() {
     KTextDocument doc = new KTextDocument();
     doc.updateText(def);
-    Assert.assertEquals("require", doc.getContextAt(new KPos(2, 2)));
+    Assert.assertEquals("requires", doc.getContextAt(new KPos(2, 2)));
     Assert.assertEquals("module", doc.getContextAt(new KPos(4, 8)));
     Assert.assertEquals("imports", doc.getContextAt(new KPos(9, 21)));
     Assert.assertEquals("syntax", doc.getContextAt(new KPos(11, 18)));
diff --git a/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java b/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java
index 58993b3c2e8..47dd298b09b 100644
--- a/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java
+++ b/kernel/src/test/java/org/kframework/parser/outer/MDsourceTest.java
@@ -17,7 +17,7 @@ public void test1() {
         "1\n"
             + " ```k\n"
             + " // ignore indentation\n"
-            + "require \"a.md\"\n"
+            + "requires \"a.md\"\n"
             + " ```\n"
             + "6\n"
             + "```{a b}\n"
@@ -43,7 +43,7 @@ public void test1() {
         "\n"
             + " \n"
             + " // ignore indentation\n"
-            + "require \"a.md\"\n"
+            + "requires \"a.md\"\n"
             + " \n"
             + "\n"
             + " \n"