change uses of .

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

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

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

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]

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]

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]

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

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

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

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

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

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

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

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

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

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

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