fixed typos
authordesharna
Thu, 17 Jun 2021 10:43:53 +0200
changeset 74112 07675be65227
parent 74111 c55980cf7374
child 74113 a88427e55371
fixed typos
src/Doc/Sledgehammer/document/root.tex
--- 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