Change {...}<:S syntax to {...}::S

k-distribution/include/kframework/builtin/domains.md

@@ -1932,7 +1932,7 @@ module STRING-BUFFER-IN-K [symbolic]
   syntax StringBuffer ::= String
   syntax String ::= StringBuffer2String ( StringBuffer ) [function, total]
 
-  rule {SB:String +String S:String}<:StringBuffer => (SB +String S)::String
+  rule {SB:String +String S:String}::StringBuffer => (SB +String S)::String
   rule .StringBuffer => ""
   rule StringBuffer2String(S:String) => S
 endmodule

k-distribution/include/kframework/builtin/kast.md

@@ -387,7 +387,7 @@ module AUTO-CASTS
   // generates, for all sorts, productions of the form:
   // Sort  ::= Sort ":Sort"  // semantic cast - force the inner term to be `Sort` or a subsort
   // Sort  ::= Sort "::Sort" // strict cast - force the inner term to be exactly `Sort`. Useful for disambiguation
-  // Sort ::= "{" Sort "}" "<:Sort" // synonym for strict cast
+  // Sort ::= "{" Sort "}" "::Sort" // synonym for strict cast
   // Sort  ::= "{" K "}"    ":>Sort" // projection cast. Allows any term to be placed in a context that expects `Sort`
   // this is part of the mechanism that allows concrete user syntax in K
 endmodule

k-distribution/k-tutorial/1_basic/11_casts/README.md

@@ -152,9 +152,9 @@ it has no effect on the sort of the subterm `I1:Int + I2:Int`.
 
 For cases like this, K provides an alternative syntax for strict casts:
 ```
-  syntax S ::= "{" S "}<:S"
+  syntax S ::= "{" S "}::S"
 ```
-The ambiguity can then be resolved with `{I1:Int + I2:Int}<:Exp` or `{I1:Int + I2:Int}<:Exp2`.
+The ambiguity can then be resolved with `{I1:Int + I2:Int}::Exp` or `{I1:Int + I2:Int}::Exp2`.
 
 ### Projection casts