src/Doc/IsarRef/Generic.thy
changeset 50070 e447ad4d6edd
parent 50068 310e9b810bbf
child 50071 959548c3b947
     1.1 --- a/src/Doc/IsarRef/Generic.thy	Sun Nov 04 20:12:01 2012 +0100
     1.2 +++ b/src/Doc/IsarRef/Generic.thy	Sun Nov 04 20:23:26 2012 +0100
     1.3 @@ -1189,7 +1189,7 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -subsection {* Automated methods *}
     1.8 +subsection {* Fully automated methods *}
     1.9  
    1.10  text {*
    1.11    \begin{matharray}{rcl}
    1.12 @@ -1324,7 +1324,7 @@
    1.13  *}
    1.14  
    1.15  
    1.16 -subsection {* Semi-automated methods *}
    1.17 +subsection {* Partially automated methods *}
    1.18  
    1.19  text {* These proof methods may help in situations when the
    1.20    fully-automated tools fail.  The result is a simpler subgoal that
    1.21 @@ -1370,9 +1370,9 @@
    1.22      @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
    1.23    \end{matharray}
    1.24  
    1.25 -  These are the primitive tactics behind the (semi)automated proof
    1.26 -  methods of the Classical Reasoner.  By calling them yourself, you
    1.27 -  can execute these procedures one step at a time.
    1.28 +  These are the primitive tactics behind the automated proof methods
    1.29 +  of the Classical Reasoner.  By calling them yourself, you can
    1.30 +  execute these procedures one step at a time.
    1.31  
    1.32    \begin{description}
    1.33