Apply suggestions from code review

Co-authored-by: Ryan Scott <[email protected]>

doc/manual/manual.md

@@ -4048,7 +4048,7 @@ of a circuit and a functional specification.  SAW enables these proofs with the
 experimental `prove_bisim` command:
 
 ~~~~
-prove_bisim : ProofScript () -> [BisimTheorem] -> Term -> Term -> Term -> Term -> TopLevel ProofResult
+prove_bisim : ProofScript () -> [BisimTheorem] -> Term -> Term -> Term -> Term -> TopLevel BisimTheorem
 ~~~~
 
 When invoking `prove_bisim strat theorems srel orel lhs rhs`, the arguments
@@ -4290,9 +4290,9 @@ The `STATE RELATION THEOREM` verifies that the output relation properly captures
 the guarantees of the state relation.  The `OUTPUT RELATION THEOREM` verifies
 that if `lhs` and `rhs` are executed with related states, then the result of
 that execution is also related.  These two theorems together guarantee that the
-terms simulate eachother.
+terms simulate each other.
 
-When using composition, the `prove_bisim` also generates and attempts to solve
+When using composition, `prove_bisim` also generates and attempts to solve
 the proof goal below for any successfully applied `BisimTheorem` in the
 `theorems` list:
 

intTests/test_bisimulation/comp.saw

@@ -4,15 +4,15 @@ import "Comp.cry";
 
 enable_experimental;
 
-// Prove 'andImp' and 'andSpec' simulate eachother
+// Prove 'andImp' and 'andSpec' simulate each other
 and_res <- prove_bisim z3
                        []
                        {{ andStateRel }}
                        {{ andOutputRel }}
                        {{ andImp }}
                        {{ andSpec }};
 
-// Prove 'nandImp' and 'nandSpec' simulate eachother, using 'and_res' in the
+// Prove 'nandImp' and 'nandSpec' simulate each other, using 'and_res' in the
 // process.
 nand_res <- prove_bisim (do {
     unfolding ["nandImp", "nandSpec"];

src/SAWScript/Bisimulation/BisimTheorem.hs

@@ -12,8 +12,8 @@ module SAWScript.Bisimulation.BisimTheorem
 import qualified Cryptol.TypeCheck.Type as C
 import Verifier.SAW.TypedTerm ( TypedTerm )
 
--- A proved bisimulation theorem.  See the comment at the top of
--- 'SAWScript.Bisimulation' for an explanation of some of the terms used here.
+-- | A proved bisimulation theorem.  See the comment at the top of
+-- "SAWScript.Bisimulation" for an explanation of some of the terms used here.
 data BisimTheorem = BisimTheorem {
     bisimTheoremStateRelation :: TypedTerm
  -- ^ State relation