src/HOL/Isar_examples/Group.thy

     by (simp only: group_left_unit);
   finally; show ?thesis; .;
 qed;
 
 text {*
- There are only two Isar language elements for calculational proofs:
- \isakeyword{also} for initial or intermediate calculational steps,
- and \isakeyword{finally} for building the result of a calculation.
- These constructs are not hardwired into Isabelle/Isar, but defined on
- top of the basic Isar/VM interpreter.  Expanding the
+ \bigskip There are only two Isar language elements for calculational
+ proofs: \isakeyword{also} for initial or intermediate calculational
+ steps, and \isakeyword{finally} for building the result of a
+ calculation.  These constructs are not hardwired into Isabelle/Isar,
+ but defined on top of the basic Isar/VM interpreter.  Expanding the
  \isakeyword{also} and \isakeyword{finally} derived language elements,
  calculations may be simulated as demonstrated below.
 
  Note that ``$\dots$'' is just a special term binding that happens to
  be bound automatically to the argument of the last fact established

 
   show ?thesis; .;
 qed;
 
 
-subsection {* Groups and monoids *};
+subsection {* Groups as monoids *};
 
 text {*
   Monoids are usually defined like this.
 *};