src/Doc/Prog_Prove/Logic.thy

 
 If you want to try all of the above automatic proof methods you simply type
 \begin{isabelle}
 \isacom{try}
 \end{isabelle}
-You can also add specific simplification and introduction rules:
+There is also a lightweight variant \isacom{try0} that does not call
+sledgehammer. If desired, specific simplification and introduction rules
+can be added:
 \begin{isabelle}
-\isacom{try} @{text"simp: \<dots> intro: \<dots>"}
+\isacom{try0} @{text"simp: \<dots> intro: \<dots>"}
 \end{isabelle}
-There is also a lightweight variant \isacom{try0} that does not call
-sledgehammer.
 
 \section{Single Step Proofs}
 
 Although automation is nice, it often fails, at least initially, and you need
 to find out why. When @{text fastforce} or @{text blast} simply fail, you have