Initial SAW Manual Reorganization

doc/saw-user-manual/creating-symbolic-variables.md

@@ -1,6 +1,6 @@
 # Creating Symbolic Variables
 
-The direct extraction process just discussed automatically introduces
+The direct extraction process discussed previously introduces
 symbolic variables and then abstracts over them, yielding a SAWScript
 `Term` that reflects the semantics of the original Java, LLVM, or MIR code.
 For simple functions, this is often the most convenient interface. For

doc/saw-user-manual/loading-code.md

@@ -213,8 +213,8 @@ linking 11 mir files into <...>/example.linked-mir.json
 
 ## Direct Extraction
 
-In the case of the `max` function described earlier, the relevant inputs
-and outputs are immediately apparent. The function takes two integer
+In many simple cases (such as the mathematical `max` function), the relevant
+inputs and outputs are immediately apparent. The function takes two integer
 arguments, always uses both of them, and returns a single integer value,
 making no other changes to the program state.
 

doc/saw-user-manual/the-term-type.md

@@ -10,4 +10,5 @@ will say more later about exactly what it means for two terms to be
 equivalent, and how to determine whether two terms are equivalent.
 
 Before exploring the `Term` type more deeply, it is important to
-understand the role of the Cryptol language in SAW.
+understand the role of the Cryptol language in SAW -- make sure to read
+[that section of the manual](./cryptol-and-its-role-in-saw) before continuing.

doc/saw-user-manual/transforming-term-values.md

@@ -3,7 +3,7 @@
 The three primary functions of SAW are _extracting_ models (`Term`
 values) from programs, _transforming_ those models, and _proving_
 properties about models using external provers. So far we've shown how
-to construct `Term` values from Cryptol programs; later sections
+to construct `Term` values from programs; later sections
 will describe how to extract them from other programs. Now we show how
 to use the various term transformation features available in SAW.