# HG changeset patch
# User desharna
# Date 1623919433 -7200
# Node ID 07675be652278238c47a66134c7bfc7242bb8443
# Parent  c55980cf7374d67b2b096d14d719b013728e6a0c
fixed typos

diff -r c55980cf7374 -r 07675be65227 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