--- a/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 10:37:29 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Thu Jun 17 10:43:53 2021 +0200
@@ -1234,7 +1234,7 @@
\label{mirabelle}
The \texttt{isabelle mirabelle} tool executes Sledgehammer or other advisory
-tools (e.g., Nitpick) or tactics (e.g., \textit{auto}) on all subgoals emering
+tools (e.g., Nitpick) or tactics (e.g., \textit{auto}) on all subgoals emerging
in a theory. It is typically used to measure the success rate of a proof tool
on some benchmark. Its command-line usage is as follows:
@@ -1271,7 +1271,7 @@
Option \texttt{-T THEORY} restricts the subgoals to those emerging from this
theory. When not provided, all subgoals from are theories are selected. When
-provided multiple times, the union of all specified theories's subgoals is
+provided multiple times, the union of all specified theories' subgoals is
selected.
Option \texttt{-m INT} specifies a maximum number of goals on which the action