From 0f8cc3752e4586a480870687ab73df64b124f302 Mon Sep 17 00:00:00 2001
From: Guy Repta <50716988+gtrepta@users.noreply.github.com>
Date: Mon, 19 Feb 2024 15:19:32 -0600
Subject: [PATCH] change uses of .

---
 1_k/2_imp/lesson_4/imp.k                      |  4 +-
 1_k/2_imp/lesson_5/imp.md                     |  4 +-
 1_k/3_lambda++/lesson_2/lambda.k              |  2 +-
 1_k/3_lambda++/lesson_3/lambda.k              |  2 +-
 1_k/3_lambda++/lesson_4/lambda.k              |  2 +-
 1_k/3_lambda++/lesson_5/lambda.k              |  2 +-
 1_k/3_lambda++/lesson_6/lambda.md             |  2 +-
 1_k/4_imp++/lesson_1/imp.k                    |  6 +--
 1_k/4_imp++/lesson_2/imp.k                    |  6 +--
 1_k/4_imp++/lesson_3/imp.k                    |  6 +--
 1_k/4_imp++/lesson_4/imp.k                    |  8 ++--
 1_k/4_imp++/lesson_5/imp.k                    | 12 ++---
 1_k/4_imp++/lesson_6/imp.k                    | 16 +++----
 1_k/4_imp++/lesson_7/imp.k                    | 16 +++----
 1_k/4_imp++/lesson_7/tests/proofs/sum-spec.k  |  8 ++--
 1_k/4_imp++/lesson_8/imp.md                   | 14 +++---
 1_k/4_imp++/lesson_8/tests/proofs/abs-spec.k  |  4 +-
 1_k/4_imp++/lesson_8/tests/proofs/max-spec.k  |  4 +-
 1_k/4_imp++/lesson_8/tests/proofs/min-spec.k  |  4 +-
 1_k/4_imp++/lesson_8/tests/proofs/sum-spec.k  |  8 ++--
 1_k/5_types/lesson_3/lambda.k                 |  2 +-
 1_k/5_types/lesson_5.5/lambda.k               |  2 +-
 1_k/5_types/lesson_5/lambda.k                 |  4 +-
 1_k/5_types/lesson_6/lambda.k                 |  4 +-
 1_k/5_types/lesson_8/lambda.k                 |  2 +-
 1_k/5_types/lesson_9/lambda.k                 |  2 +-
 .../1_simple/1_untyped/simple-untyped.md      | 34 +++++++-------
 .../2_typed/2_dynamic/simple-typed-dynamic.md | 34 +++++++-------
 2_languages/2_kool/1_untyped/kool-untyped.md  | 44 +++++++++---------
 .../2_typed/1_dynamic/kool-typed-dynamic.md   | 46 +++++++++----------
 .../2_typed/2_static/kool-typed-static.md     | 26 +++++------
 .../1_untyped/1_environment/fun-untyped.md    | 14 +++---
 32 files changed, 172 insertions(+), 172 deletions(-)

diff --git a/1_k/2_imp/lesson_4/imp.k b/1_k/2_imp/lesson_4/imp.k
index 35c69649..3fc116bf 100644
--- a/1_k/2_imp/lesson_4/imp.k
+++ b/1_k/2_imp/lesson_4/imp.k
@@ -46,10 +46,10 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .
+  rule {} => .K
   rule {S} => S
 // Stmt
-  rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
+  rule <k> X = I:Int; => .K ...</k> <state>... X |-> (_ => I) ...</state>
   rule S1:Stmt S2:Stmt => S1 ~> S2
   rule if (true)  S else _ => S
   rule if (false) _ else S => S
diff --git a/1_k/2_imp/lesson_5/imp.md b/1_k/2_imp/lesson_5/imp.md
index b4715158..26a0a1b8 100644
--- a/1_k/2_imp/lesson_5/imp.md
+++ b/1_k/2_imp/lesson_5/imp.md
@@ -155,7 +155,7 @@ contents, thus effectively giving them a bracket semantics; we can afford to
 do this only because we have no block-local variable declarations yet in IMP.
 
 ```k
-  rule {} => .
+  rule {} => .K
   rule {S} => S
 ```
 
@@ -165,7 +165,7 @@ to be declared, otherwise the semantics will get stuck.  At the same time,
 the assignment is dissolved.
 
 ```k
-  rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
+  rule <k> X = I:Int; => .K ...</k> <state>... X |-> (_ => I) ...</state>
 ```
 
 ### Sequential composition
diff --git a/1_k/3_lambda++/lesson_2/lambda.k b/1_k/3_lambda++/lesson_2/lambda.k
index 70207f54..c684fbee 100644
--- a/1_k/3_lambda++/lesson_2/lambda.k
+++ b/1_k/3_lambda++/lesson_2/lambda.k
@@ -27,5 +27,5 @@ module LAMBDA
        <store>... N |-> V ...</store>
 
 // Auxiliary task
-  rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
+  rule <k> _:Val ~> (Rho => .K) ...</k> <env> _ => Rho </env>
 endmodule
diff --git a/1_k/3_lambda++/lesson_3/lambda.k b/1_k/3_lambda++/lesson_3/lambda.k
index c6ebf44c..3b52935f 100644
--- a/1_k/3_lambda++/lesson_3/lambda.k
+++ b/1_k/3_lambda++/lesson_3/lambda.k
@@ -25,7 +25,7 @@ module LAMBDA
   rule <k> X => V ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> V ...</store>
-  rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
+  rule <k> _:Val ~> (Rho => .K) ...</k> <env> _ => Rho </env>
 
   syntax Val ::= Int | Bool
   syntax Exp ::= Exp "*" Exp          [strict, left]
diff --git a/1_k/3_lambda++/lesson_4/lambda.k b/1_k/3_lambda++/lesson_4/lambda.k
index 4a5e2240..7802a038 100644
--- a/1_k/3_lambda++/lesson_4/lambda.k
+++ b/1_k/3_lambda++/lesson_4/lambda.k
@@ -25,7 +25,7 @@ module LAMBDA
   rule <k> X => V ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> V ...</store>
-  rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
+  rule <k> _:Val ~> (Rho => .K) ...</k> <env> _ => Rho </env>
 
   syntax Val ::= Int | Bool
   syntax Exp ::= Exp "*" Exp          [strict, left]
diff --git a/1_k/3_lambda++/lesson_5/lambda.k b/1_k/3_lambda++/lesson_5/lambda.k
index cd9e9213..d51ecb3d 100644
--- a/1_k/3_lambda++/lesson_5/lambda.k
+++ b/1_k/3_lambda++/lesson_5/lambda.k
@@ -26,7 +26,7 @@ module LAMBDA
   rule <k> X => V ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> V ...</store>
-  rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
+  rule <k> _:Val ~> (Rho => .K) ...</k> <env> _ => Rho </env>
 
   syntax Val ::= Int | Bool
   syntax Exp ::= Exp "*" Exp          [strict, left]
diff --git a/1_k/3_lambda++/lesson_6/lambda.md b/1_k/3_lambda++/lesson_6/lambda.md
index 466bb86a..664ac3a1 100644
--- a/1_k/3_lambda++/lesson_6/lambda.md
+++ b/1_k/3_lambda++/lesson_6/lambda.md
@@ -126,7 +126,7 @@ semantics, like it was above. It is so useful, that there are discussions
 in the **K** team to add it to the set of pre-defined **K** features.
 
 ```k
-  rule <k> _:Val ~> (Rho => .) ...</k> <env> _ => Rho </env>
+  rule <k> _:Val ~> (Rho => .K) ...</k> <env> _ => Rho </env>
 ```
 
 ### Arithmetic Constructs
diff --git a/1_k/4_imp++/lesson_1/imp.k b/1_k/4_imp++/lesson_1/imp.k
index 8ea2df0e..4125b96f 100644
--- a/1_k/4_imp++/lesson_1/imp.k
+++ b/1_k/4_imp++/lesson_1/imp.k
@@ -55,10 +55,10 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .
+  rule {} => .K
   rule {S} => S
 // Stmt
-  rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
+  rule <k> X = I:Int; => .K ...</k> <state>... X |-> (_ => I) ...</state>
   rule S1:Stmt S2:Stmt => S1 ~> S2
   rule if (true)  S else _ => S
   rule if (false) _ else S => S
@@ -67,5 +67,5 @@ module IMP
   rule <k> int (X,Xs => Xs); ...</k>
        <state> Rho (.Map => X |-> 0) </state>
     requires notBool (X in keys(Rho))
-  rule int .Ids; => .
+  rule int .Ids; => .K
 endmodule
diff --git a/1_k/4_imp++/lesson_2/imp.k b/1_k/4_imp++/lesson_2/imp.k
index 700741a8..2872acd7 100644
--- a/1_k/4_imp++/lesson_2/imp.k
+++ b/1_k/4_imp++/lesson_2/imp.k
@@ -57,10 +57,10 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .
+  rule {} => .K
   rule {S} => S
 // Stmt
-  rule <k> X = I:Int; => . ...</k>
+  rule <k> X = I:Int; => .K ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
   rule S1:Stmt S2:Stmt => S1 ~> S2
@@ -71,5 +71,5 @@ module IMP
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .
+  rule int .Ids; => .K
 endmodule
diff --git a/1_k/4_imp++/lesson_3/imp.k b/1_k/4_imp++/lesson_3/imp.k
index f6f73fc0..fa7db5c8 100644
--- a/1_k/4_imp++/lesson_3/imp.k
+++ b/1_k/4_imp++/lesson_3/imp.k
@@ -60,10 +60,10 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .
+  rule {} => .K
   rule {S} => S
 // Stmt
-  rule <k> X = I:Int; => . ...</k>
+  rule <k> X = I:Int; => .K ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
   rule S1:Stmt S2:Stmt => S1 ~> S2
@@ -74,5 +74,5 @@ module IMP
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .
+  rule int .Ids; => .K
 endmodule
diff --git a/1_k/4_imp++/lesson_4/imp.k b/1_k/4_imp++/lesson_4/imp.k
index c5fbb14b..71ae12f0 100644
--- a/1_k/4_imp++/lesson_4/imp.k
+++ b/1_k/4_imp++/lesson_4/imp.k
@@ -65,10 +65,10 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .
+  rule {} => .K
   rule {S} => S
 // Stmt
-  rule <k> X = I:Int; => . ...</k>
+  rule <k> X = I:Int; => .K ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
   rule S1:Stmt S2:Stmt => S1 ~> S2
@@ -79,7 +79,7 @@ module IMP
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .
+  rule int .Ids; => .K
 
   syntax Printable ::= Int | String
 /* currently it is necessary to subsort Printable to AExp,
@@ -88,5 +88,5 @@ module IMP
   context print(HOLE:AExp, _);
   rule <k> print(P:Printable,AEs => AEs); ...</k>
        <output>... .List => ListItem(P) </output>
-  rule print(.AExps); => .
+  rule print(.AExps); => .K
 endmodule
diff --git a/1_k/4_imp++/lesson_5/imp.k b/1_k/4_imp++/lesson_5/imp.k
index 98034792..f8215325 100644
--- a/1_k/4_imp++/lesson_5/imp.k
+++ b/1_k/4_imp++/lesson_5/imp.k
@@ -64,11 +64,11 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .
+  rule {} => .K
   rule <k> {S} => S ~> Rho ...</k> <env> Rho </env>
-  rule <k> Rho => . ...</k> <env> _ => Rho </env>
+  rule <k> Rho => .K ...</k> <env> _ => Rho </env>
 // Stmt
-  rule <k> X = I:Int; => . ...</k>
+  rule <k> X = I:Int; => .K ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
   rule S1:Stmt S2:Stmt => S1 ~> S2
@@ -79,7 +79,7 @@ module IMP
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .
+  rule int .Ids; => .K
 
   syntax Printable ::= Int | String
 /* currently it is necessary to subsort Printable to AExp,
@@ -88,7 +88,7 @@ module IMP
   context print(HOLE:AExp, _AEs:AExps);
   rule <k> print(P:Printable,AEs => AEs); ...</k>
        <output>... .List => ListItem(P) </output>
-  rule print(.AExps); => .
+  rule print(.AExps); => .K
 
-  rule <k> halt; ~> _ => . </k>
+  rule <k> halt; ~> _ => .K </k>
 endmodule
diff --git a/1_k/4_imp++/lesson_6/imp.k b/1_k/4_imp++/lesson_6/imp.k
index f9da2c27..8e382390 100644
--- a/1_k/4_imp++/lesson_6/imp.k
+++ b/1_k/4_imp++/lesson_6/imp.k
@@ -70,11 +70,11 @@ module IMP
   rule true && B => B
   rule false && _ => false
 // Block
-  rule {} => .
+  rule {} => .K
   rule <k> {S} => S ~> Rho ...</k> <env> Rho </env>
-  rule <k> Rho => . ...</k> <env> _ => Rho </env>
+  rule <k> Rho => .K ...</k> <env> _ => Rho </env>
 // Stmt
-  rule <k> X = I:Int; => . ...</k>
+  rule <k> X = I:Int; => .K ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
   rule S1:Stmt S2:Stmt => S1 ~> S2
@@ -85,7 +85,7 @@ module IMP
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .
+  rule int .Ids; => .K
 
   syntax Printable ::= Int | String
 /* currently it is necessary to subsort Printable to AExp,
@@ -94,12 +94,12 @@ module IMP
   context print(HOLE:AExp, _AEs:AExps);
   rule <k> print(P:Printable,AEs => AEs); ...</k>
        <output>... .List => ListItem(P) </output>
-  rule print(.AExps); => .
+  rule print(.AExps); => .K
 
-  rule <k> halt; ~> _ => . </k>
+  rule <k> halt; ~> _ => .K </k>
 
-  rule <k> spawn S => . ...</k> <env> Rho </env>
+  rule <k> spawn S => .K ...</k> <env> Rho </env>
        (.Bag => <thread>... <k> S </k> <env> Rho </env> <id> !_T:Int +Int 1 </id> ...</thread>)
 
-  rule <thread>... <k> . </k> ...</thread> => .Bag
+  rule <thread>... <k> .K </k> ...</thread> => .Bag
 endmodule
diff --git a/1_k/4_imp++/lesson_7/imp.k b/1_k/4_imp++/lesson_7/imp.k
index 7b393cfa..56967795 100644
--- a/1_k/4_imp++/lesson_7/imp.k
+++ b/1_k/4_imp++/lesson_7/imp.k
@@ -72,9 +72,9 @@ module IMP
   rule false && _ => false
 // Block
   rule <k> {Ss} => Ss ~> Rho ...</k> <env> Rho </env>
-  rule <k> Rho => . ...</k> <env> _ => Rho </env>
+  rule <k> Rho => .K ...</k> <env> _ => Rho </env>
 // Stmt
-  rule _:Int; => .
+  rule _:Int; => .K
   rule <k> X = I:Int => I ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
@@ -85,7 +85,7 @@ module IMP
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .
+  rule int .Ids; => .K
 
   syntax Printable ::= Int | String
 /* currently it is necessary to subsort Printable to AExp,
@@ -94,17 +94,17 @@ module IMP
   context print(HOLE:AExp, _AEs:AExps);
   rule <k> print(P:Printable,AEs => AEs); ...</k>
        <output>... .List => ListItem(P) </output>
-  rule print(.AExps); => .
+  rule print(.AExps); => .K
 
-  rule <k> halt; ~> _ => . </k>
+  rule <k> halt; ~> _ => .K </k>
 
   rule <k> spawn S => !T:Int +Int 1 ...</k> <env> Rho </env>
        (.Bag => <thread>... <k> S </k> <env> Rho </env> <id> !T +Int 1 </id> ...</thread>)
-  rule <k> join(T:Int); => . ...</k>
-       <thread>... <k> . </k> <id> T </id> ...</thread>
+  rule <k> join(T:Int); => .K ...</k>
+       <thread>... <k> .K </k> <id> T </id> ...</thread>
 
 // Stmts
-  rule .Stmts => .
+  rule .Stmts => .K
   rule S:Stmt Ss:Stmts => S ~> Ss
 
 // verification ids
diff --git a/1_k/4_imp++/lesson_7/tests/proofs/sum-spec.k b/1_k/4_imp++/lesson_7/tests/proofs/sum-spec.k
index f46213e3..902adc45 100644
--- a/1_k/4_imp++/lesson_7/tests/proofs/sum-spec.k
+++ b/1_k/4_imp++/lesson_7/tests/proofs/sum-spec.k
@@ -19,14 +19,14 @@ claim
     ...</env>
   ...</thread></threads>
   <input>
-    ListItem ( #buffer ( "\n" ~> . ) )
+    ListItem ( #buffer ( "\n" ~> .K ) )
     ListItem ( "off" )
     ListItem ( #istream ( 0 ) )
   </input>
   <output>
     ListItem ( #ostream ( 1 ) )
     ListItem ( "off" )
-    ListItem ( #buffer ( "" ~> . ) )
+    ListItem ( #buffer ( "" ~> .K ) )
   </output>
   <store>...
     LN   |-> (N:Int => 0)
@@ -56,14 +56,14 @@ claim
     </env>
   ...</thread></threads>
   <input>
-    ListItem ( #buffer ( "\n" ~> . ) )
+    ListItem ( #buffer ( "\n" ~> .K ) )
     ListItem ( "off" )
     ListItem ( #istream ( 0 ) )
   </input>
   <output>
     ListItem ( #ostream ( 1 ) )
     ListItem ( "off" )
-    ListItem ( #buffer ( "" ~> . ) )
+    ListItem ( #buffer ( "" ~> .K ) )
   </output>
   <store>
     .Map
diff --git a/1_k/4_imp++/lesson_8/imp.md b/1_k/4_imp++/lesson_8/imp.md
index e6181194..78b26a18 100644
--- a/1_k/4_imp++/lesson_8/imp.md
+++ b/1_k/4_imp++/lesson_8/imp.md
@@ -324,7 +324,7 @@ this syntactic restructuring has been explained in Lesson 7. Here is the
 semantics of the two constructs:
 
 ```k
-  rule _:Int; => .
+  rule _:Int; => .K
   rule <k> X = I:Int => I ...</k>
        <env>... X |-> N ...</env>
        <store>... N |-> (_ => I) ...</store>
@@ -338,7 +338,7 @@ sequentialize a syntactic list of statements `s1 s2 ... sn..` into the
 corresponding computation `s1 ~> s2 ~> ... ~> sn`.
 
 ```k
-   rule .Stmts => .
+   rule .Stmts => .K
    rule S:Stmt Ss:Stmts => S ~> Ss
 ```
 
@@ -423,7 +423,7 @@ compete on the output buffer.
 
   rule <k> print(P:Printable,AEs => AEs); ...</k>
        <output>... .List => ListItem(P) </output>
-  rule print(.AExps); => .
+  rule print(.AExps); => .K
 ```
 
 ### Halt
@@ -437,7 +437,7 @@ terminates the entire program, no matter how many concurrent threads it has,
 because there is nothing else to rewrite.
 
 ```k
-  rule <k> halt; ~> _ => . </k>
+  rule <k> halt; ~> _ => .K </k>
 ```
 
 ### Spawn thread
@@ -477,7 +477,7 @@ join statement is simply dissolved. The terminated thread is not removed,
 because we want to allow possible other join statements to also dissolve.
 
 ```k
-  rule <k> join(T); => . ...</k> <thread>... <k>.</k> <id>T</id> ...</thread>
+  rule <k> join(T); => .K ...</k> <thread>... <k>.K</k> <id>T</id> ...</thread>
 ```
 
 ### Blocks
@@ -513,7 +513,7 @@ initialize it with 0.
   rule <k> int (X,Xs => Xs); ...</k>
        <env> Rho => Rho[X <- !N:Int] </env>
        <store>... .Map => !N |-> 0 ...</store>
-  rule int .Ids; => .
+  rule int .Ids; => .K
 ```
 
 ### Auxiliary operations
@@ -522,7 +522,7 @@ recovery. Its role is to discard the current environment in the
 `env` cell and replace it with the environment that it holds.
 
 ```k
-  rule <k> Rho => . ...</k> <env> _ => Rho </env>
+  rule <k> Rho => .K ...</k> <env> _ => Rho </env>
 ```
 
 If you want to avoid useless environment recovery steps and keep the size
diff --git a/1_k/4_imp++/lesson_8/tests/proofs/abs-spec.k b/1_k/4_imp++/lesson_8/tests/proofs/abs-spec.k
index c06a5d79..1368edd7 100644
--- a/1_k/4_imp++/lesson_8/tests/proofs/abs-spec.k
+++ b/1_k/4_imp++/lesson_8/tests/proofs/abs-spec.k
@@ -20,14 +20,14 @@ claim
     ...</env>
   ...</thread></threads>
   <input>
-    ListItem ( #buffer ( "\n" ~> . ) )
+    ListItem ( #buffer ( "\n" ~> .K ) )
     ListItem ( "off" )
     ListItem ( #istream ( 0 ) )
   </input>
   <output>
     ListItem ( #ostream ( 1 ) )
     ListItem ( "off" )
-    ListItem ( #buffer ( "" ~> . ) )
+    ListItem ( #buffer ( "" ~> .K ) )
   </output>
   <store>...
     LA |-> A:Int
diff --git a/1_k/4_imp++/lesson_8/tests/proofs/max-spec.k b/1_k/4_imp++/lesson_8/tests/proofs/max-spec.k
index bb3e430a..7c07987a 100644
--- a/1_k/4_imp++/lesson_8/tests/proofs/max-spec.k
+++ b/1_k/4_imp++/lesson_8/tests/proofs/max-spec.k
@@ -21,14 +21,14 @@ claim
     ...</env>
   ...</thread></threads>
   <input>
-    ListItem ( #buffer ( "\n" ~> . ) )
+    ListItem ( #buffer ( "\n" ~> .K ) )
     ListItem ( "off" )
     ListItem ( #istream ( 0 ) )
   </input>
   <output>
     ListItem ( #ostream ( 1 ) )
     ListItem ( "off" )
-    ListItem ( #buffer ( "" ~> . ) )
+    ListItem ( #buffer ( "" ~> .K ) )
   </output>
   <store>...
     LA |-> A:Int
diff --git a/1_k/4_imp++/lesson_8/tests/proofs/min-spec.k b/1_k/4_imp++/lesson_8/tests/proofs/min-spec.k
index 892ac78f..96c1bdb1 100644
--- a/1_k/4_imp++/lesson_8/tests/proofs/min-spec.k
+++ b/1_k/4_imp++/lesson_8/tests/proofs/min-spec.k
@@ -21,14 +21,14 @@ claim
     ...</env>
   ...</thread></threads>
   <input>
-    ListItem ( #buffer ( "\n" ~> . ) )
+    ListItem ( #buffer ( "\n" ~> .K ) )
     ListItem ( "off" )
     ListItem ( #istream ( 0 ) )
   </input>
   <output>
     ListItem ( #ostream ( 1 ) )
     ListItem ( "off" )
-    ListItem ( #buffer ( "" ~> . ) )
+    ListItem ( #buffer ( "" ~> .K ) )
   </output>
   <store>...
     LA |-> A:Int
diff --git a/1_k/4_imp++/lesson_8/tests/proofs/sum-spec.k b/1_k/4_imp++/lesson_8/tests/proofs/sum-spec.k
index a9c9aca9..122c8472 100644
--- a/1_k/4_imp++/lesson_8/tests/proofs/sum-spec.k
+++ b/1_k/4_imp++/lesson_8/tests/proofs/sum-spec.k
@@ -19,14 +19,14 @@ claim
     ...</env>
   ...</thread></threads>
   <input>
-    ListItem ( #buffer ( "\n" ~> . ) )
+    ListItem ( #buffer ( "\n" ~> .K ) )
     ListItem ( "off" )
     ListItem ( #istream ( 0 ) )
   </input>
   <output>
     ListItem ( #ostream ( 1 ) )
     ListItem ( "off" )
-    ListItem ( #buffer ( "" ~> . ) )
+    ListItem ( #buffer ( "" ~> .K ) )
   </output>
   <store>...
     LN   |-> (N:Int => 0)
@@ -61,14 +61,14 @@ claim
     </env>
   ...</thread></threads>
   <input>
-    ListItem ( #buffer ( "\n" ~> . ) )
+    ListItem ( #buffer ( "\n" ~> .K ) )
     ListItem ( "off" )
     ListItem ( #istream ( 0 ) )
   </input>
   <output>
     ListItem ( #ostream ( 1 ) )
     ListItem ( "off" )
-    ListItem ( #buffer ( "" ~> . ) )
+    ListItem ( #buffer ( "" ~> .K ) )
   </output>
   <store>...
     .Map
diff --git a/1_k/5_types/lesson_3/lambda.k b/1_k/5_types/lesson_3/lambda.k
index cb0c80c7..9a0203f9 100644
--- a/1_k/5_types/lesson_3/lambda.k
+++ b/1_k/5_types/lesson_3/lambda.k
@@ -54,5 +54,5 @@ module LAMBDA
        <tenv> Rho => Rho[X <- T] </tenv>
 
 // Auxiliary type environment recovery
-  rule <k> _:Type ~> (Rho => .) ...</k> <tenv> _ => Rho </tenv>
+  rule <k> _:Type ~> (Rho => .K) ...</k> <tenv> _ => Rho </tenv>
 endmodule
diff --git a/1_k/5_types/lesson_5.5/lambda.k b/1_k/5_types/lesson_5.5/lambda.k
index 9824bdbe..2e5b49d3 100644
--- a/1_k/5_types/lesson_5.5/lambda.k
+++ b/1_k/5_types/lesson_5.5/lambda.k
@@ -50,5 +50,5 @@ module LAMBDA
 
   rule let X = E in E' => (lambda X . E') E
 
-  rule <k> _T:Type ~> (env(TEnv:Map) => .) ...</k> <tenv> _:Map => TEnv </tenv>
+  rule <k> _T:Type ~> (env(TEnv:Map) => .K) ...</k> <tenv> _:Map => TEnv </tenv>
 endmodule
diff --git a/1_k/5_types/lesson_5/lambda.k b/1_k/5_types/lesson_5/lambda.k
index 04591db4..8ff03840 100644
--- a/1_k/5_types/lesson_5/lambda.k
+++ b/1_k/5_types/lesson_5/lambda.k
@@ -45,8 +45,8 @@ module LAMBDA
        <tenv> TEnv => TEnv[X <- ?T] </tenv>
 
   syntax KItem ::= Type "=" Type
-  rule T = T => .
+  rule T = T => .K
 
   syntax KItem ::= setTenv(Map)
-  rule <k> _T:Type ~> (setTenv(TEnv) => .) ...</k>  <tenv> _ => TEnv </tenv>
+  rule <k> _T:Type ~> (setTenv(TEnv) => .K) ...</k>  <tenv> _ => TEnv </tenv>
 endmodule
diff --git a/1_k/5_types/lesson_6/lambda.k b/1_k/5_types/lesson_6/lambda.k
index 1c90573b..7e99c1cc 100644
--- a/1_k/5_types/lesson_6/lambda.k
+++ b/1_k/5_types/lesson_6/lambda.k
@@ -65,7 +65,7 @@ module LAMBDA
        (.Bag => <task> <k> E = ?T </k> <tenv> TEnv[X <- ?T] </tenv> </task>)
 
   syntax KItem ::= Exp "=" Exp  [seqstrict]
-  rule <k> T:Type = T:Type => . ...</k>
+  rule <k> T:Type = T:Type => .K ...</k>
 
-  rule <task>... <k> . </k> ...</task> => .Bag
+  rule <task>... <k> .K </k> ...</task> => .Bag
 endmodule
diff --git a/1_k/5_types/lesson_8/lambda.k b/1_k/5_types/lesson_8/lambda.k
index cbfedb21..0744acac 100644
--- a/1_k/5_types/lesson_8/lambda.k
+++ b/1_k/5_types/lesson_8/lambda.k
@@ -56,5 +56,5 @@ module LAMBDA
   rule T = T => .
 
   syntax KItem ::= setTenv(Map)
-  rule <k> _T:Type ~> (setTenv(TEnv) => .) ...</k>  <tenv> _ => TEnv </tenv>
+  rule <k> _T:Type ~> (setTenv(TEnv) => .K) ...</k>  <tenv> _ => TEnv </tenv>
 endmodule
diff --git a/1_k/5_types/lesson_9/lambda.k b/1_k/5_types/lesson_9/lambda.k
index d16780e5..a9ee1d87 100644
--- a/1_k/5_types/lesson_9/lambda.k
+++ b/1_k/5_types/lesson_9/lambda.k
@@ -65,5 +65,5 @@ module LAMBDA
   rule T = T => .
 
   syntax KItem ::= setTenv(Map)
-  rule <k> _T:Type ~> (setTenv(TEnv) => .) ...</k>  <tenv> _ => TEnv </tenv>
+  rule <k> _T:Type ~> (setTenv(TEnv) => .K) ...</k>  <tenv> _ => TEnv </tenv>
 endmodule
diff --git a/2_languages/1_simple/1_untyped/simple-untyped.md b/2_languages/1_simple/1_untyped/simple-untyped.md
index 1f215fce..ecfa8324 100644
--- a/2_languages/1_simple/1_untyped/simple-untyped.md
+++ b/2_languages/1_simple/1_untyped/simple-untyped.md
@@ -440,7 +440,7 @@ structure.
 ```k
   syntax KItem ::= "undefined"  [latex(\bot)]
 
-  rule <k> var X:Id; => . ...</k>
+  rule <k> var X:Id; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> undefined ...</store>
        <nextLoc> L => L +Int 1 </nextLoc>
@@ -467,7 +467,7 @@ declarations.
 ```k
   context var _:Id[HOLE];
 
-  rule <k> var X:Id[N:Int]; => . ...</k>
+  rule <k> var X:Id[N:Int]; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> array(L +Int 1, N)
                           (L +Int 1) ... (L +Int N) |-> undefined ...</store>
@@ -528,7 +528,7 @@ SIMPLE, also defined in **K** (see `examples/simple/typed/static`),
 discards programs which do not respect this requirement.
 
 ```k
-  rule <k> function F(Xs) S => . ...</k>
+  rule <k> function F(Xs) S => .K ...</k>
        <env> Env => Env[F <- L] </env>
        <store>... .Map => L |-> lambda(Xs, S) ...</store>
        <nextLoc> L => L +Int 1 </nextLoc>
@@ -774,7 +774,7 @@ for variable declarations, as we did above.  One can make the two rules below
 computational if one wants them to count as computational steps.
 
 ```k
-  rule {} => .
+  rule {} => .K
   rule <k> { S } => S ~> setEnv(Env) ...</k>  <env> Env </env>
 ```
 The basic definition of environment recovery is straightforward and
@@ -834,7 +834,7 @@ Expression statements are only used for their side effects, so their result
 value is simply discarded.  Common examples of expression statements are ones
 of the form `++x;`, `x=e;`, `e1[e2]=e3;`, etc.
 ```k
-  rule _:Val; => .
+  rule _:Val; => .K
 ```
 
 ## Conditional
@@ -868,7 +868,7 @@ its evaluated arguments to the output buffer, and discard the residual
 `print` statement with an empty list of arguments.
 ```k
   rule <k> print(V:Val, Es => Es); ...</k> <output>... .List => ListItem(V) </output>
-  rule print(.Vals); => .
+  rule print(.Vals); => .K
 ```
 
 ## Exceptions
@@ -909,7 +909,7 @@ exception stack.  The three rules below modularly do precisely the above.
        </control>
        <env> Env </env>
 
-  rule <k> popx => . ...</k>
+  rule <k> popx => .K ...</k>
        <xstack> ListItem(_) => .List ...</xstack>
 
   rule <k> throw V:Val; ~> _ => { var X = V; S2 } ~> K </k>
@@ -971,7 +971,7 @@ by a thread.  The unique identifier of the terminated thread is also collected
 into the `terminated` cell, so the `join` construct knows which
 threads have terminated.
 ```k
-  rule (<thread>... <k>.</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
+  rule (<thread>... <k>.K</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
        <busy> Busy => Busy -Set keys(H) </busy>
        <terminated>... .Set => SetItem(T) ...</terminated>
 ```
@@ -983,7 +983,7 @@ the identifier of the thread to be joined is in the `terminated` cell.
 If yes, then the `join` statement dissolves and the joining thread
 continues normally; if not, then the joining thread gets stuck.
 ```k
-  rule <k> join T:Int; => . ...</k>
+  rule <k> join T:Int; => .K ...</k>
        <terminated>... SetItem(T) ...</terminated>
 ```
 
@@ -998,12 +998,12 @@ the side condition of the first rule).
 counter for the lock (the locks are re-entrant).  These two cases are captured
 by the two rules below:
 ```k
-  rule <k> acquire V:Val; => . ...</k>
+  rule <k> acquire V:Val; => .K ...</k>
        <holds>... .Map => V |-> 0 ...</holds>
        <busy> Busy (.Set => SetItem(V)) </busy>
     requires (notBool(V in Busy))
 
-  rule <k> acquire V; => . ...</k>
+  rule <k> acquire V; => .K ...</k>
        <holds>... V:Val |-> (N => N +Int 1) ...</holds>
 ```
 
@@ -1017,11 +1017,11 @@ is to decrement the lock counter.
 from its `holds` cell and also from the the shared `busy` cell,
 so other threads can acquire it if they need to.
 ```k
-  rule <k> release V:Val; => . ...</k>
+  rule <k> release V:Val; => .K ...</k>
        <holds>... V |-> (N => N -Int 1) ...</holds>
     requires N >Int 0
 
-  rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
+  rule <k> release V; => .K ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
        <busy>... SetItem(V) => .Set ...</busy>
 ```
 
@@ -1042,8 +1042,8 @@ the `thread` cell, the only way to concretize the rule below to the
 actual configuration of SIMPLE is to include each `k` cell in a
 `thread` cell.
 ```k
-  rule <k> rendezvous V:Val; => . ...</k>
-       <k> rendezvous V; => . ...</k>
+  rule <k> rendezvous V:Val; => .K ...</k>
+       <k> rendezvous V; => .K ...</k>
 ```
 
 ## Auxiliary declarations and operations
@@ -1078,7 +1078,7 @@ IMP++ tutorial:
 // TODO: eliminate the env wrapper, like we did in IMP++
 
   syntax KItem ::= setEnv(Map)
-  rule <k> setEnv(Env) => . ...</k> <env> _ => Env </env>
+  rule <k> setEnv(Env) => .K ...</k> <env> _ => Env </env>
 ```
 While theoretically sufficient, the basic definition for environment
 recovery alone is suboptimal.  Consider a loop `while (E)S`,
@@ -1093,7 +1093,7 @@ recovery tasks, we only need to keep the last one.  The elegant rule below
 does precisely that, thus avoiding the unnecessary computation explosion
 problem:
 ```k
-  rule (setEnv(_) => .) ~> setEnv(_)
+  rule (setEnv(_) => .K) ~> setEnv(_)
 ```
 In fact, the above follows a common convention in **K** for recovery
 operations of cell contents: the meaning of a computation task of the form
diff --git a/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md b/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md
index 292e7187..15262040 100644
--- a/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md
+++ b/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md
@@ -224,7 +224,7 @@ to a location.
 ```k
   syntax KItem ::= undefined(Type)  [latex(\bot_{#1})]
 
-  rule <k> T:Type X:Id; => . ...</k>
+  rule <k> T:Type X:Id; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> undefined(T) ...</store>
        <nextLoc> L:Int => L +Int 1 </nextLoc>
@@ -236,7 +236,7 @@ The dynamic semantics of typed array declarations is similar to that
 in untyped SIMPLE, but we have to make sure that we associate the
 right type to the allocated locations.
 ```k
-  rule <k> T:Type X:Id[N:Int]; => . ...</k>
+  rule <k> T:Type X:Id[N:Int]; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> array(T, L +Int 1, N)
                           (L +Int 1)...(L +Int N) |-> undefined(T) ...</store>
@@ -271,7 +271,7 @@ Store all function parameters, as well as the return type, as part
 of the lambda abstraction.  In the spirit of dynamic typing, we will
 make sure that parameters are well typed when the function is invoked.
 ```k
-  rule <k> T:Type F:Id(Ps:Params) S => . ...</k>
+  rule <k> T:Type F:Id(Ps:Params) S => .K ...</k>
        <env> Env => Env[F <- L] </env>
        <store>... .Map => L |-> lambda(T, Ps, S) ...</store>
        <nextLoc> L => L +Int 1 </nextLoc>
@@ -404,7 +404,7 @@ preserved:
 ### Blocks
 
 ```k
-  rule {} => .
+  rule {} => .K
   rule <k> { S } => S ~> setEnv(Env) ...</k>  <env> Env </env>
 ```
 
@@ -417,7 +417,7 @@ preserved:
 ### Expression statements
 
 ```k
-  rule _:Val; => .
+  rule _:Val; => .K
 ```
 
 ### Conditional
@@ -439,7 +439,7 @@ We only allow printing integers and strings:
 ```k
   rule <k> print(V:Val, Es => Es); ...</k> <output>... .List => ListItem(V) </output>
     requires typeOf(V) ==K int orBool typeOf(V) ==K string
-  rule print(.Vals); => .
+  rule print(.Vals); => .K
 ```
 
 ### Exceptions
@@ -461,7 +461,7 @@ values, in which case our semantics below works fine:
        </control>
        <env> Env </env>
 
-  rule <k> popx => . ...</k>
+  rule <k> popx => .K ...</k>
        <xstack> ListItem(_) => .List ...</xstack>
 
   rule <k> throw V:Val; ~> _ => { T X = V; S2 } ~> K </k>
@@ -491,7 +491,7 @@ values, in which case our semantics below works fine:
 ### Thread termination
 
 ```k
-   rule (<thread>... <k>.</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
+   rule (<thread>... <k>.K</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
         <busy> Busy => Busy -Set keys(H) </busy>
         <terminated>... .Set => SetItem(T) ...</terminated>
 ```
@@ -499,38 +499,38 @@ values, in which case our semantics below works fine:
 ### Thread joining
 
 ```k
-   rule <k> join T:Int; => . ...</k>
+   rule <k> join T:Int; => .K ...</k>
         <terminated>... SetItem(T) ...</terminated>
 ```
 
 ### Acquire lock
 
 ```k
-   rule <k> acquire V:Val; => . ...</k>
+   rule <k> acquire V:Val; => .K ...</k>
         <holds>... .Map => V |-> 0 ...</holds>
         <busy> Busy (.Set => SetItem(V)) </busy>
      requires (notBool(V in Busy:Set))
 
-   rule <k> acquire V; => . ...</k>
+   rule <k> acquire V; => .K ...</k>
         <holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
 ```
 
 ### Release lock
 
 ```k
-   rule <k> release V:Val; => . ...</k>
+   rule <k> release V:Val; => .K ...</k>
         <holds>... V |-> (N => N:Int -Int 1) ...</holds>
       requires N >Int 0
 
-   rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
+   rule <k> release V; => .K ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
         <busy>... SetItem(V) => .Set ...</busy>
 ```
 
 ### Rendezvous synchronization
 
 ```k
-   rule <k> rendezvous V:Val; => . ...</k>
-        <k> rendezvous V; => . ...</k>
+   rule <k> rendezvous V:Val; => .K ...</k>
+        <k> rendezvous V; => .K ...</k>
 ```
 
 ### Auxiliary declarations and operations
@@ -553,8 +553,8 @@ Environment recovery.
 // TODO: same comment regarding setEnv(...) as for simple untyped
 
   syntax KItem ::= setEnv(Map)
-  rule <k> setEnv(Env) => . ...</k>  <env> _ => Env </env>
-  rule (setEnv(_) => .) ~> setEnv(_)
+  rule <k> setEnv(Env) => .K ...</k>  <env> _ => Env </env>
+  rule (setEnv(_) => .K) ~> setEnv(_)
 ```
 lvalue and loc
 ```k
diff --git a/2_languages/2_kool/1_untyped/kool-untyped.md b/2_languages/2_kool/1_untyped/kool-untyped.md
index 593e33c2..ea1dc286 100644
--- a/2_languages/2_kool/1_untyped/kool-untyped.md
+++ b/2_languages/2_kool/1_untyped/kool-untyped.md
@@ -383,7 +383,7 @@ definition.
 ```k
   syntax KItem ::= "undefined"  [latex(\bot)]
 
-  rule <k> var X:Id; => . ...</k>
+  rule <k> var X:Id; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> undefined ...</store>
        <nextLoc> L:Int => L +Int 1 </nextLoc>
@@ -391,7 +391,7 @@ definition.
 
   context var _:Id[HOLE];
 
-  rule <k> var X:Id[N:Int]; => . ...</k>
+  rule <k> var X:Id[N:Int]; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> array(L +Int 1, N)
                           (L +Int 1) ... (L +Int N) |-> undefined ...</store>
@@ -475,13 +475,13 @@ interestingly, the semantics of return stays unchanged.
 
   rule <k> loc(L) = V:Val => V ...</k> <store>... L |-> (_ => V) ...</store>
 
-  rule {} => .
+  rule {} => .K
   rule <k> { S } => S ~> setEnv(Env) ...</k>  <env> Env </env>
 
 
   rule S1::Stmt S2::Stmt => S1 ~> S2
 
-  rule _:Val; => .
+  rule _:Val; => .K
 
   rule if ( true) S else _ => S
   rule if (false) _ else S => S
@@ -489,7 +489,7 @@ interestingly, the semantics of return stays unchanged.
   rule while (E) S => if (E) {S while(E)S}
 
   rule <k> print(V:Val, Es => Es); ...</k> <output>... .List => ListItem(V) </output>
-  rule print(.Vals); => .
+  rule print(.Vals); => .K
 
 
   syntax KItem ::= xstackFrame(Id,Stmt,K,Map,K)
@@ -505,7 +505,7 @@ interestingly, the semantics of return stays unchanged.
        </control>
        <env> Env </env>
 
-  rule <k> popx => . ...</k>
+  rule <k> popx => .K ...</k>
        <xstack> ListItem(_) => .List ...</xstack>
 
   rule <k> throw V:Val; ~> _ => { var X = V; S2 } ~> K </k>
@@ -522,33 +522,33 @@ interestingly, the other concurrency constructs keep their semantics
 from SIMPLE unchanged.
 ```k
   // TODO(KORE): ..Bag should be . throughout this definition #1772
-  rule (<thread>... <k>.</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
+  rule (<thread>... <k>.K</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
   /*
   rule (<thread>... <k>.</k> <holds>H</holds> <id>T</id> ...</thread> => .)
   */
        <busy> Busy => Busy -Set keys(H) </busy>
        <terminated>... .Set => SetItem(T) ...</terminated>
 
-  rule <k> join T:Int; => . ...</k>
+  rule <k> join T:Int; => .K ...</k>
        <terminated>... SetItem(T) ...</terminated>
 
-  rule <k> acquire V:Val; => . ...</k>
+  rule <k> acquire V:Val; => .K ...</k>
        <holds>... .Map => V |-> 0 ...</holds>
        <busy> Busy (.Set => SetItem(V)) </busy>
     requires (notBool(V in Busy:Set))
 
-  rule <k> acquire V; => . ...</k>
+  rule <k> acquire V; => .K ...</k>
        <holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
 
-  rule <k> release V:Val; => . ...</k>
+  rule <k> release V:Val; => .K ...</k>
        <holds>... V |-> (N => N:Int -Int 1) ...</holds>
     requires N >Int 0
 
-  rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
+  rule <k> release V; => .K ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
        <busy>... SetItem(V) => .Set ...</busy>
 
-  rule <k> rendezvous V:Val; => . ...</k>
-       <k> rendezvous V; => . ...</k>
+  rule <k> rendezvous V:Val; => .K ...</k>
+       <k> rendezvous V; => .K ...</k>
 ```
 
 ## Unchanged auxiliary operations from untyped SIMPLE
@@ -566,8 +566,8 @@ from SIMPLE unchanged.
   rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store>
 
   syntax KItem ::= setEnv(Map)
-  rule <k> setEnv(Env) => . ...</k>  <env> _ => Env </env>
-  rule (setEnv(_) => .) ~> setEnv(_)
+  rule <k> setEnv(Env) => .K ...</k>  <env> _ => Env </env>
+  rule (setEnv(_) => .K) ~> setEnv(_)
   // TODO: How can we make sure that the second rule above applies before the first one?
   //       Probably we'll deal with this using strategies, eventually.
 
@@ -703,7 +703,7 @@ environment.
 Initially, the classes forming the program are moved into their
 corresponding cells:
 ```k
-  rule <k> class Class1 extends Class2 { S } => . ...</k>
+  rule <k> class Class1 extends Class2 { S } => .K ...</k>
        <classes>... (.Bag => <classData>
                             <className> Class1 </className>
                             <baseClass> Class2 </baseClass>
@@ -729,7 +729,7 @@ This gives the KOOL programmer a lot of power; one should use this
 power wisely, though, because programs can become easily hard to
 understand and reason about if one overuses these features.
 ```k
-  rule <k> method F:Id(Xs:Ids) S => . ...</k>
+  rule <k> method F:Id(Xs:Ids) S => .K ...</k>
        <crntClass> Class:Id </crntClass>
        <location> OL:Int </location>
        <env> Env => Env[F <- L] </env>
@@ -788,7 +788,7 @@ members (both fields and methods) of that class.
        <baseClass> Class1:Id </baseClass>
        <declarations> S </declarations>
 
-  rule <k> create(Object) => . ...</k>
+  rule <k> create(Object) => .K ...</k>
 ```
 The next operation sets the current class of the current object.
 This is necessary to be done at each layer, because the current class
@@ -797,7 +797,7 @@ semantics of method declarations above).
 ```k
   syntax KItem ::= setCrntClass(Id)
 
-  rule <k> setCrntClass(C) => . ...</k>
+  rule <k> setCrntClass(C) => .K ...</k>
        <crntClass> _ => C </crntClass>
 ```
 The next operation adds a new tagged environment layer to the
@@ -807,7 +807,7 @@ empty).
 ```k
   syntax KItem ::= "addEnvLayer"
 
-  rule <k> addEnvLayer => . ...</k>
+  rule <k> addEnvLayer => .K ...</k>
        <env> Env => .Map </env>
        <crntClass> Class:Id </crntClass>
        <envStack> .List => ListItem(envStackFrame(Class, Env)) ...</envStack>
@@ -822,7 +822,7 @@ the location is unnecessary and thus we delete it from the
 ```k
   syntax KItem ::= "storeObj"
 
-  rule <k> storeObj => . ...</k>
+  rule <k> storeObj => .K ...</k>
        <crntObj> <crntClass> CC </crntClass> <envStack> ES </envStack> (<location> L:Int </location> => .Bag) </crntObj>
        <store>... .Map => L |-> objectClosure(CC, ES) ...</store>
 ```
diff --git a/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md b/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md
index 2befbe64..a2f79c68 100644
--- a/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md
+++ b/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md
@@ -249,13 +249,13 @@ KOOL).
 
   syntax KItem ::= undefined(Type)  [latex(\bot_{#1})]
 
-  rule <k> T:Type X:Id; => . ...</k>
+  rule <k> T:Type X:Id; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> undefined(T) ...</store>
        <nextLoc> L:Int => L +Int 1 </nextLoc>
 
 
-  rule <k> T:Type X:Id[N:Int]; => . ...</k>
+  rule <k> T:Type X:Id[N:Int]; => .K ...</k>
        <env> Env => Env[X <- L] </env>
        <store>... .Map => L |-> array(T, L +Int 1, N)
                           (L +Int 1)...(L +Int N) |-> undefined(T) ...</store>
@@ -326,14 +326,14 @@ KOOL).
   context (HOLE => lvalue(HOLE)) = _
 
 
-  rule {} => .
+  rule {} => .K
   rule <k> { S } => S ~> setEnv(Env) ...</k>  <env> Env </env>
 
 
   rule S1:Stmt S2:Stmt => S1 ~> S2
 
 
-  rule _:Val; => .
+  rule _:Val; => .K
 
 
   rule if ( true) S else _ => S
@@ -345,33 +345,33 @@ KOOL).
 
   rule <k> print(V:Val, Es => Es); ...</k> <output>... .List => ListItem(V) </output>
     requires typeOf(V) ==K int orBool typeOf(V) ==K string
-  rule print(.Vals); => .
+  rule print(.Vals); => .K
 
 
-  rule (<thread>... <k>.</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
+  rule (<thread>... <k>.K</k> <holds>H</holds> <id>T</id> ...</thread> => .Bag)
        <busy> Busy => Busy -Set keys(H) </busy>
        <terminated>... .Set => SetItem(T) ...</terminated>
 
-  rule <k> join T:Int; => . ...</k>
+  rule <k> join T:Int; => .K ...</k>
        <terminated>... SetItem(T) ...</terminated>
 
-  rule <k> acquire V:Val; => . ...</k>
+  rule <k> acquire V:Val; => .K ...</k>
        <holds>... .Map => V |-> 0 ...</holds>
        <busy> Busy (.Set => SetItem(V)) </busy>
     requires (notBool(V in Busy:Set))
 
-  rule <k> acquire V; => . ...</k>
+  rule <k> acquire V; => .K ...</k>
        <holds>... V:Val |-> (N:Int => N +Int 1) ...</holds>
 
-  rule <k> release V:Val; => . ...</k>
+  rule <k> release V:Val; => .K ...</k>
        <holds>... V |-> (N => N:Int -Int 1) ...</holds>
     requires N >Int 0
 
-  rule <k> release V; => . ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
+  rule <k> release V; => .K ...</k> <holds>... V:Val |-> 0 => .Map ...</holds>
        <busy>... SetItem(V) => .Set ...</busy>
 
-  rule <k> rendezvous V:Val; => . ...</k>
-       <k> rendezvous V; => . ...</k>
+  rule <k> rendezvous V:Val; => .K ...</k>
+       <k> rendezvous V; => .K ...</k>
 ```
 
 ## Unchanged auxiliary operations from dynamically typed SIMPLE
@@ -386,8 +386,8 @@ KOOL).
   rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store>
 
   syntax KItem ::= setEnv(Map)
-  rule <k> setEnv(Env) => . ...</k>  <env> _ => Env </env>
-  rule (setEnv(_) => .) ~> setEnv(_)
+  rule <k> setEnv(Env) => .K ...</k>  <env> _ => Env </env>
+  rule (setEnv(_) => .K) ~> setEnv(_)
 
   syntax Exp ::= lvalue(K)
   syntax Val ::= loc(Int)
@@ -532,7 +532,7 @@ encountered.
        </control>
        <env> Env </env>
 
-  rule <k> popx => . ...</k>
+  rule <k> popx => .K ...</k>
        <xstack> ListItem(_) => .List ...</xstack>
 
   rule <k> throw V:Val; ~> _
@@ -568,7 +568,7 @@ Like in untyped KOOL.
 
 Like in untyped KOOL.
 ```k
-  rule <k> class Class1 extends Class2 { S } => . ...</k>
+  rule <k> class Class1 extends Class2 { S } => .K ...</k>
        <classes>... (.Bag => <classData>
                             <className> Class1 </className>
                             <baseClass> Class2 </baseClass>
@@ -584,7 +584,7 @@ closures, so that their type contract can be checked at invocation
 time.  The rule below is conceptually similar to that of untyped KOOL;
 the only difference is the addition of the types.
 ```k
-  rule <k> T:Type F:Id(Ps:Params) S => . ...</k>
+  rule <k> T:Type F:Id(Ps:Params) S => .K ...</k>
        <crntClass> C </crntClass>
        <location> OL </location>
        <env> Env => Env[F <- L] </env>
@@ -628,23 +628,23 @@ those in untyped KOOL.
        <baseClass> Class1:Id </baseClass>
        <declarations> S </declarations>
 
-  rule <k> create(Object) => . ...</k>
+  rule <k> create(Object) => .K ...</k>
 
   syntax KItem ::= setCrntClass(Id)
 
-  rule <k> setCrntClass(C) => . ...</k>
+  rule <k> setCrntClass(C) => .K ...</k>
        <crntClass> _ => C </crntClass>
 
   syntax KItem ::= "addEnvLayer"
 
-  rule <k> addEnvLayer => . ...</k>
+  rule <k> addEnvLayer => .K ...</k>
        <env> Env => .Map </env>
        <crntClass> Class:Id </crntClass>
        <envStack> .List => ListItem(envStackFrame(Class, Env)) ...</envStack>
 
   syntax KItem ::= "storeObj"
 
-  rule <k> storeObj => . ...</k>
+  rule <k> storeObj => .K ...</k>
        <crntObj>
          <crntClass> Class </crntClass>
          <envStack> EStack </envStack>
@@ -863,7 +863,7 @@ A generic computational guard: it allows the computation to continue
 only if a prefix guard evaluates to true.
 ```k
   syntax KItem ::= "true?"
-  rule true ~> true? => .
+  rule true ~> true? => .K
 
 endmodule
 ```
diff --git a/2_languages/2_kool/2_typed/2_static/kool-typed-static.md b/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
index 7d06610e..76018c12 100644
--- a/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
+++ b/2_languages/2_kool/2_typed/2_static/kool-typed-static.md
@@ -823,9 +823,9 @@ The subclass relation introduces a subtyping relation.
 ```k
   syntax KItem ::= checkSubtype(Types,Types)
 
-  rule checkSubtype(T:Type, T) => .
+  rule checkSubtype(T:Type, T) => .K
 
-  rule <k> checkSubtype(`class`(C:Id), `class`(C':Id)) => . ...</k>
+  rule <k> checkSubtype(`class`(C:Id), `class`(C':Id)) => .K ...</k>
        <className> C </className>
        <baseClasses>... SetItem(C') ...</baseClasses>
 
@@ -839,8 +839,8 @@ The subclass relation introduces a subtyping relation.
     => checkSubtype(T,T') ~> checkSubtype(Ts,Ts')
     requires Ts =/=K .Types
 
-  rule checkSubtype(.Types,.Types) => .
-  rule checkSubtype(.Types,void) => .
+  rule checkSubtype(.Types,.Types) => .K
+  rule checkSubtype(.Types,void) => .K
 ```
 
 ## Checking well-formedness of types
@@ -852,13 +852,13 @@ check that the types used in the program actually exists
 
   rule checkType(T:Type,Ts:Types) => checkType(T) ~> checkType(Ts)
     requires Ts =/=K .Types
-  rule checkType(.Types) => .
-  rule checkType(int) => .
-  rule checkType(bool) => .
-  rule checkType(string) => .
-  rule checkType(void) => .
-  rule <k> checkType(`class`(C:Id)) => . ...</k> <className> C </className>
-  rule checkType(`class`(Object)) => .
+  rule checkType(.Types) => .K
+  rule checkType(int) => .K
+  rule checkType(bool) => .K
+  rule checkType(string) => .K
+  rule checkType(void) => .K
+  rule <k> checkType(`class`(C:Id)) => .K ...</k> <className> C </className>
+  rule checkType(`class`(Object)) => .K
   rule checkType(Ts:Types -> T:Type) => checkType(T,Ts)
   rule checkType(T:Type[]) => checkType(T)
 ```
@@ -885,7 +885,7 @@ is co-variant in the codomain and contra-variant in the domain).
        <ctenv> Rho </ctenv>
     requires notBool(F in keys(Rho))
 
-  rule checkMethod(_:Id,_,Object) => .
+  rule checkMethod(_:Id,_,Object) => .K
 ```
 
 ## Generic operations which could be part of the **K** framework
@@ -894,7 +894,7 @@ is co-variant in the codomain and contra-variant in the domain).
   syntax KItem ::= stuck(K)  [latex(\framebox{${#1}$})]
 
   syntax KItem ::= "discard"
-  rule _:KResult ~> discard => .
+  rule _:KResult ~> discard => .K
 
 endmodule
 ```
diff --git a/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md b/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
index 04393e3d..28085e29 100644
--- a/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
+++ b/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
@@ -563,11 +563,11 @@ making sure that the environment is properly recovered afterwards.
 If the first pattern does not match, then we drop it and thus move on
 to the next one.
 ```k
-  rule (. => getMatching(P, V)) ~> closure(_, P->_ | _) V:Val
+  rule (.K => getMatching(P, V)) ~> closure(_, P->_ | _) V:Val
   rule <k> matchResult(M:Map) ~> closure(Rho, _->E | _) _
            => bindMap(M) ~> E ~> setEnv(Rho') ...</k>
        <env> Rho' => Rho </env>
-  rule (matchFailure => .) ~> closure(_, (_->_ | Cs:Cases => Cs)) _
+  rule (matchFailure => .K) ~> closure(_, (_->_ | Cs:Cases => Cs)) _
 //  rule <k> closure(Rho, P->E | _) V:Val
 //           => bindMap(getMatching(P,V)) ~> E ~> setEnv(Rho') ...</k>
 //       <env> Rho' => Rho </env>  when isMatching(P,V)
@@ -694,7 +694,7 @@ way to achieve the benefits of tail recursion in **K**.
 ```k
   syntax KItem ::= setEnv(Map)  // TODO: get rid of env
   //rule (setEnv(_) => .) ~> setEnv(_)  [anywhere]
-  rule <k> _:Val ~> (setEnv(Rho) => .) ...</k> <env> _ => Rho </env>
+  rule <k> _:Val ~> (setEnv(Rho) => .K) ...</k> <env> _ => Rho </env>
 ```
 
 ## `bindTo`, `bind` and `assignTo`
@@ -707,21 +707,21 @@ above.
                  | bindMap(Map)
                  | bind(Names)
 
-  rule (. => getMatchingAux(Xs,Vs)) ~> bindTo(Xs:Names,Vs:Vals)
+  rule (.K => getMatchingAux(Xs,Vs)) ~> bindTo(Xs:Names,Vs:Vals)
   rule matchResult(M:Map) ~> bindTo(_:Names, _:Vals) => bindMap(M)
 
-  rule bindMap(.Map) => .
+  rule bindMap(.Map) => .K
   rule <k> bindMap((X:Name |-> V:Val => .Map) _:Map) ...</k>
        <env> Rho => Rho[X <- !L:Int] </env>
        <store>... .Map => !L |-> V ...</store>
 
-  rule bind(.Names) => .
+  rule bind(.Names) => .K
   rule <k> bind(X:Name,Xs => Xs) ...</k>
        <env> Rho => Rho[X <- !_L:Int] </env>
 
   syntax KItem ::= assignTo(Names,Exps)  [strict(2)]
 
-  rule <k> assignTo(.Names,.Vals) => . ...</k>
+  rule <k> assignTo(.Names,.Vals) => .K ...</k>
   rule <k> assignTo((X:Name,Xs => Xs),(V:Val,Vs:Vals => Vs)) ...</k>
        <env>... X |-> L ...</env>
        <store>... .Map => L |-> V ...</store>