Use keyword claim in integration tests (#2280)

Author: MirceaS

test/all-path/00-basic/00-no-rules/distinct-spec.k

@@ -8,6 +8,6 @@ module DISTINCT-SPEC
   imports PATH
 
   // should not be provable, as there is no axiom
-  rule <k> a => b </k> [all-path]
+  claim <k> a => b </k> [all-path]
 
 endmodule

test/all-path/00-basic/00-no-rules/identity-spec.k

@@ -7,6 +7,6 @@ module IDENTITY-SPEC
   imports VERIFICATION
   imports PATH
 
-  rule <k> a => a </k> [all-path]
+  claim <k> a => a </k> [all-path]
 
 endmodule

test/all-path/00-basic/01-one-rule/all-path-b-or-c-spec.k

@@ -7,6 +7,6 @@ module ALL-PATH-B-OR-C-SPEC
   import PATH
 
   // This should be provable as transiting to b suffices
-  rule <k> a => b #Or c </k> [all-path]
+  claim <k> a => b #Or c </k> [all-path]
 
 endmodule

test/all-path/00-basic/01-one-rule/all-path-b-spec.k

@@ -7,6 +7,6 @@ module ALL-PATH-B-SPEC
   imports PATH
 
   // This should be provable as there is only one axiom.
-  rule <k> a => b </k> [all-path]
+  claim <k> a => b </k> [all-path]
 
 endmodule

test/all-path/00-basic/01-one-rule/all-path-c-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-C-SPEC
   imports PATH
 
   // This should not be provable as the only axiom is a => b.
-  rule <k> a => c </k> [all-path]
+  claim <k> a => c </k> [all-path]
 
 endmodule

test/all-path/00-basic/02-cyclic-rule/all-path-b-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-B-SPEC
   imports PATH
 
   // Everything is provable if I can reach a cycling rule
-  rule <k> a => b </k> [all-path]
+  claim <k> a => b </k> [all-path]
 
 endmodule

test/all-path/00-basic/02-cyclic-rule/all-path-c-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-C-SPEC
   imports PATH
 
   // Everything is provable if I can reach a cycling rule
-  rule <k> a => c </k> [all-path]
+  claim <k> a => c </k> [all-path]
 
 endmodule

test/all-path/00-basic/03-concurrent-rules/all-path-b-or-c-spec.k

@@ -8,6 +8,6 @@ module ALL-PATH-B-OR-C-SPEC
   imports PATH
 
 // This should be provable as both one-path and all-path.
-  rule <k> a => b #Or c </k> [all-path]
+  claim <k> a => b #Or c </k> [all-path]
 
 endmodule

test/all-path/00-basic/03-concurrent-rules/all-path-b-spec.k

@@ -9,6 +9,6 @@ module ALL-PATH-B-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an 
   //all-path claim.
-  rule <k> a => c </k> [all-path]
+  claim <k> a => c </k> [all-path]
 
 endmodule

test/all-path/00-basic/03-concurrent-rules/one-path-b-spec.k

@@ -9,6 +9,6 @@ module ONE-PATH-B-SPEC
 
   // This should be provable as an one-path claim, but should not be provable as an 
   //all-path claim.
-  rule <k> a => c </k> [one-path]
+  claim <k> a => c </k> [one-path]
 
 endmodule