avoid clash of terminology wrt. "semi-automated" in the sense of Isar (e.g. method "rule");
--- a/src/Doc/IsarRef/Generic.thy Sun Nov 04 20:12:01 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Sun Nov 04 20:23:26 2012 +0100
@@ -1189,7 +1189,7 @@
*}
-subsection {* Automated methods *}
+subsection {* Fully automated methods *}
text {*
\begin{matharray}{rcl}
@@ -1324,7 +1324,7 @@
*}
-subsection {* Semi-automated methods *}
+subsection {* Partially automated methods *}
text {* These proof methods may help in situations when the
fully-automated tools fail. The result is a simpler subgoal that
@@ -1370,9 +1370,9 @@
@{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
\end{matharray}
- These are the primitive tactics behind the (semi)automated proof
- methods of the Classical Reasoner. By calling them yourself, you
- can execute these procedures one step at a time.
+ These are the primitive tactics behind the automated proof methods
+ of the Classical Reasoner. By calling them yourself, you can
+ execute these procedures one step at a time.
\begin{description}