# HG changeset patch
# User desharna
# Date 1639986028 -3600
# Node ID 953f53f03437f1d8f5f4d7525654f76239906ee8
# Parent  089eeaaee525430f356eebeaad4115b59713e3af
updated Mirabelle documentation

diff -r 089eeaaee525 -r 953f53f03437 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Dec 20 08:14:41 2021 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Dec 20 08:40:28 2021 +0100
@@ -1293,18 +1293,18 @@
 
 \begin{verbatim}
 isabelle mirabelle -d $AFP -O output \
-  -A "sledgehammer[prover=e, prover_timeout=30]" \
+  -A "sledgehammer[provers = e, timeout = 30]" \
   VeriComp
 \end{verbatim}
 
 This command specifies to run the Sledgehammer action, using the E prover with
-a timeout of 10 seconds, on all subgoals emerging from all theory in the AFP
+a timeout of 30 seconds, on all subgoals emerging from all theory in the AFP
 session VeriComp. The results are written to \texttt{output/mirabelle.log}.
 
 \begin{verbatim}
 isabelle mirabelle -d $AFP -O output \
   -T Semantics -T Compiler \
-  -A "sledgehammer[prover=e, prover_timeout=30]" \
+  -A "sledgehammer[provers = e, timeout = 30]" \
   VeriComp
 \end{verbatim}
 
@@ -1328,7 +1328,7 @@
 
 \begin{verbatim}
 isabelle mirabelle -d $AFP -O output \
-  -A "sledgehammer[prover=e, prover_timeout=5, keep=true]" \
+  -A "sledgehammer[provers = e, timeout = 5, keep = true]" \
   VeriComp
 \end{verbatim}