deploy: 61bb5d3

docs/adr/018adr-inlining.html

@@ -268,7 +268,7 @@ <h2><a class="header" href="#options" id="options">Options</a></h2>
 <li>
 <p>Perform no inlining in preprocessing and inline only as needed in the rewriting rules.</p>
 <ul>
-<li>Pros: Spec intermediate output remains small, since inlining increases the size of the specificaiton</li>
+<li>Pros: Spec intermediate output remains small, since inlining increases the size of the specification</li>
 <li>Cons: 
 <ul>
 <li>Fewer optimizations can be applied, as some are only applicable to the syntactic forms obtained after inlining (e.g. <code>ConstSimplifier</code> can simplify <code>IF TRUE THEN a ELSE b</code>, but not <code>IF p THEN a ELSE b</code>)</li>

docs/print.html

@@ -1937,7 +1937,7 @@ <h2><a class="header" href="#tip-1-use-tla-constructs-instead-of-explicit-iterat
 
 </code></pre>
 <p>Our version of <code>NextFast</code> is quite concise and it uses the good parts of
-TLA+. However, new TLA+ users would probably write it differenty. Below you
+TLA+. However, new TLA+ users would probably write it differently. Below you
 can see the version that is more likely to be written by a specification
 writer who has good experience in software engineering:</p>
 <pre><code class="language-tla">\* Uniformly advance the clocks and update the drifts.
@@ -16400,7 +16400,7 @@ <h2><a class="header" href="#options-4" id="options-4">Options</a></h2>
 <li>
 <p>Perform no inlining in preprocessing and inline only as needed in the rewriting rules.</p>
 <ul>
-<li>Pros: Spec intermediate output remains small, since inlining increases the size of the specificaiton</li>
+<li>Pros: Spec intermediate output remains small, since inlining increases the size of the specification</li>
 <li>Cons: 
 <ul>
 <li>Fewer optimizations can be applied, as some are only applicable to the syntactic forms obtained after inlining (e.g. <code>ConstSimplifier</code> can simplify <code>IF TRUE THEN a ELSE b</code>, but not <code>IF p THEN a ELSE b</code>)</li>

docs/tutorials/trail-tips.html

@@ -242,7 +242,7 @@ <h2><a class="header" href="#tip-1-use-tla-constructs-instead-of-explicit-iterat
 
 </code></pre>
 <p>Our version of <code>NextFast</code> is quite concise and it uses the good parts of
-TLA+. However, new TLA+ users would probably write it differenty. Below you
+TLA+. However, new TLA+ users would probably write it differently. Below you
 can see the version that is more likely to be written by a specification
 writer who has good experience in software engineering:</p>
 <pre><code class="language-tla">\* Uniformly advance the clocks and update the drifts.