Enhancements to the documentation

Author: thk123

jbmc/src/java_bytecode/README.md

@@ -8,19 +8,20 @@ This module provides a front end for Java.
 To be documented.
 \subsection java-bytecode-lowering-to-goto Lowering to GOTO
 
-The Java language contains high level programming concepts like virtual functions and throw/catch semantics. We need to rewrite these in terms of other, more fundamental operations in order to analyse it. This operation is referred to as "lowering".
+The Java language contains high-level programming concepts like virtual functions and throw/catch semantics. These need to be rewritten in terms of other, more fundamental operations in order to analyse the Java program. This operation is referred to as "lowering".
 
-The following lowering operations are done on java bytecode after converting into a basic codet representation.
+The following lowering operations are done on Java bytecode after converting into a basic `codet` representation.
 
 - \ref java-bytecode-runtime-exceptions "Add runtime exceptions"
 - \ref java-bytecode-remove-java-new "Remove new calls"
 - \ref java-bytecode-remove-exceptions "Remove thrown exceptions"
+- \ref java-bytecode-remove-instance-of
 - As well as other non-java specific transformations (see \ref goto-programs for details on these)
 
 These are performed in `process_goto_function` for example
 \ref jbmc_parse_optionst::process_goto_function
 
-Once these lowerings have been completed, you have a GOTO model that can be analysed.
+Once these lowerings have been completed, you have a GOTO model that can be handled by \ref goto-symex.
 
 \section java-bytecode-object-factory Object Factory