Deploy to GitHub Pages on develop: 1cf7fc097374fcefb5b4e191bb12bdd8cf…

…94e2c5

develop/book/003_example.html

@@ -555,13 +555,13 @@ <h2 id="sec:gui">Graphical User Interface</h2>
       <code>Client_1( S, k )</code> and <code>KU( k )</code>, both of
       which are premises for the rules in the unfinished current
       constraint system.</p>
-      <p>Note that that the proof methods in the GUI are sorted
-      according to the same heuristic as is used by the
-      <code>autoprove</code> command. Any proof found by always
-      selecting the first proof method will be identical to the one
-      constructed by the <code>autoprove</code> command. However,
-      because the general problem is undecidable, the algorithm may not
-      terminate for every protocol and property.</p>
+      <p>Note that the proof methods in the GUI are sorted according to
+      the same heuristic as is used by the <code>autoprove</code>
+      command. Any proof found by always selecting the first proof
+      method will be identical to the one constructed by the
+      <code>autoprove</code> command. However, because the general
+      problem is undecidable, the algorithm may not terminate for every
+      protocol and property.</p>
       <p>In this example, both by clicking multiple times on the first
       constraint or by using the autoprover, we end with the following
       final state, where the constructed graph leads to a contradiction