core: Sequential composition uses subgoals too

kframework · Feb 11, 2020 · fed7bf9 · fed7bf9
1 parent 9394d72
commit fed7bf9
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/prover/strategies/core.md b/prover/strategies/core.md
@@ -63,10 +63,11 @@ cooled back into the sequence strategy.
 
 ```k
   syntax ResultStrategy ::= "#hole"
-  rule <strategy> S1 . S2 => S1 ~> #hole . S2 ... </strategy>
+  rule <strategy> S1 . S2 => S1 ~> #hole . S2 </strategy>
     requires notBool(isResultStrategy(S1))
      andBool notBool(isSequenceStrategy(S1))
-  rule <strategy> S1:ResultStrategy ~> #hole . S2 => S1 . S2 ... </strategy>
+  rule <claim> GOAL:Pattern </claim>
+       <strategy> S1:ResultStrategy ~> #hole . S2 => subgoal(GOAL, S1 . S2) </strategy>
 ```
 
 The `noop` (no operation) strategy is the unit for sequential composition: