docs: style: [squash] feedback from Corey

Signed-off-by: Rafal Kolanski <[email protected]>

docs/Style.thy

@@ -93,7 +93,7 @@ section \<open>Indentation\<close>
 
 text \<open>
   Isabelle code is much easier to maintain when indented consistently.
-  When in doubt, and not constrained by vertically aligning items or subgoal-count offsets, use
+  When in doubt and not constrained by vertically aligning items or subgoal-count offsets, use
   2 spaces when indenting something with respect to its container (see ``General layout`` in
   ``Other`` section).
 
@@ -400,15 +400,20 @@ term "
 section \<open>Wrapping/indenting complex rule instantiations, usually as part of @{text "_tac"} methods\<close>
 
 text \<open>
-  For simple instantiations, they can fit it on one line, like so.
+  This section concerns @{text "_tac"} methods, which are generally used when the instantiations
+  contain bound variables. When bound variables do no occur, prefer instantiations via attribute
+  (@{text "fact[where ...]"}) as they are more general.\<close>
+
+text \<open>
+  For simple instantiations which can fit it on one line, style them as follows.
   Notes:
     * for single-variable instantiations, do not use quotes
     * no space between @{text "="} and the instantiation or start of quote\<close>
 
 lemma
   "\<lbrakk>a; b\<rbrakk> \<Longrightarrow> a \<and> b"
-  apply (frule_tac P=a and Q="id b" in conjI) \<comment> \<open>when @{text a} and @{text b} contain bound vars\<close>
-  apply (frule_tac P="a" and Q= "id b" in conjI) \<comment> \<open>BAD: unnecessary quotes, unnecessary spacing\<close>
+  apply (frule_tac P=a and Q="id b" in conjI) \<comment> \<open>GOOD\<close>
+  apply (frule_tac P="a" and Q = "id b" in conjI) \<comment> \<open>BAD: unnecessary quotes, unnecessary spacing\<close>
   oops
 
 text \<open>