# HG changeset patch
# User wenzelm
# Date 1353177992 -3600
# Node ID f171b5240c31fb9ec3121827bda1ce7066c62bc2
# Parent  289181e3e524dcfdfa58265e9cca69c7ddb7cd3f
method setup for Classical steps;

diff -r 289181e3e524 -r f171b5240c31 src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Sat Nov 17 17:55:52 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Sat Nov 17 19:46:32 2012 +0100
@@ -1753,7 +1753,7 @@
   It is deterministic, with at most one outcome.
 
   \item @{method clarify} performs a series of safe steps without
-  splitting subgoals; see also @{ML clarify_step_tac}.
+  splitting subgoals; see also @{method clarify_step}.
 
   \item @{method clarsimp} acts like @{method clarify}, but also does
   simplification.  Note that if the Simplifier context includes a
@@ -1766,13 +1766,13 @@
 subsection {* Single-step tactics *}
 
 text {*
-  \begin{mldecls}
-    @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
-    @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
-    @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
-    @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
-    @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
-  \end{mldecls}
+  \begin{matharray}{rcl}
+    @{method_def safe_step} & : & @{text method} \\
+    @{method_def inst_step} & : & @{text method} \\
+    @{method_def step} & : & @{text method} \\
+    @{method_def slow_step} & : & @{text method} \\
+    @{method_def clarify_step} & : &  @{text method} \\
+  \end{matharray}
 
   These are the primitive tactics behind the automated proof methods
   of the Classical Reasoner.  By calling them yourself, you can
@@ -1780,30 +1780,30 @@
 
   \begin{description}
 
-  \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
-  subgoal @{text i}.  The safe wrapper tacticals are applied to a
-  tactic that may include proof by assumption or Modus Ponens (taking
-  care not to instantiate unknowns), or substitution.
+  \item @{method safe_step} performs a safe step on the first subgoal.
+  The safe wrapper tacticals are applied to a tactic that may include
+  proof by assumption or Modus Ponens (taking care not to instantiate
+  unknowns), or substitution.
 
-  \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
+  \item @{method inst_step} is like @{method safe_step}, but allows
   unknowns to be instantiated.
 
-  \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
-  procedure.  The unsafe wrapper tacticals are applied to a tactic
-  that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
-  rule from the context.
+  \item @{method step} is the basic step of the proof procedure, it
+  operates on the first subgoal.  The unsafe wrapper tacticals are
+  applied to a tactic that tries @{method safe}, @{method inst_step},
+  or applies an unsafe rule from the context.
 
-  \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
-  backtracking between using safe rules with instantiation (@{ML
-  inst_step_tac}) and using unsafe rules.  The resulting search space
-  is larger.
+  \item @{method slow_step} resembles @{method step}, but allows
+  backtracking between using safe rules with instantiation (@{method
+  inst_step}) and using unsafe rules.  The resulting search space is
+  larger.
 
-  \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
-  on subgoal @{text i}.  No splitting step is applied; for example,
-  the subgoal @{text "A \<and> B"} is left as a conjunction.  Proof by
-  assumption, Modus Ponens, etc., may be performed provided they do
-  not instantiate unknowns.  Assumptions of the form @{text "x = t"}
-  may be eliminated.  The safe wrapper tactical is applied.
+  \item @{method clarify_step} performs a safe step on the first
+  subgoal; no splitting step is applied.  For example, the subgoal
+  @{text "A \<and> B"} is left as a conjunction.  Proof by assumption,
+  Modus Ponens, etc., may be performed provided they do not
+  instantiate unknowns.  Assumptions of the form @{text "x = t"} may
+  be eliminated.  The safe wrapper tactical is applied.
 
   \end{description}
 *}
@@ -1839,10 +1839,10 @@
   The classical reasoning tools --- except @{method blast} --- allow
   to modify this basic proof strategy by applying two lists of
   arbitrary \emph{wrapper tacticals} to it.  The first wrapper list,
-  which is considered to contain safe wrappers only, affects @{ML
-  safe_step_tac} and all the tactics that call it.  The second one,
-  which may contain unsafe wrappers, affects the unsafe parts of @{ML
-  step_tac}, @{ML slow_step_tac}, and the tactics that call them.  A
+  which is considered to contain safe wrappers only, affects @{method
+  safe_step} and all the tactics that call it.  The second one, which
+  may contain unsafe wrappers, affects the unsafe parts of @{method
+  step}, @{method slow_step}, and the tactics that call them.  A
   wrapper transforms each step of the search, for example by
   attempting other tactics before or after the original step tactic.
   All members of a wrapper list are applied in turn to the respective
diff -r 289181e3e524 -r f171b5240c31 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Sat Nov 17 17:55:52 2012 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Sat Nov 17 19:46:32 2012 +0100
@@ -468,7 +468,7 @@
 (* fields are integral domains *)
 
 lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
-  apply (tactic "step_tac @{context} 1")
+  apply step
   apply (rule_tac a = " (a*b) * inverse b" in box_equals)
     apply (rule_tac [3] refl)
    prefer 2
diff -r 289181e3e524 -r f171b5240c31 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Nov 17 17:55:52 2012 +0100
+++ b/src/Provers/classical.ML	Sat Nov 17 19:46:32 2012 +0100
@@ -948,7 +948,17 @@
       >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
     "classical prover (iterative deepening)" #>
   Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
-    "classical prover (apply safe rules)";
+    "classical prover (apply safe rules)" #>
+  Method.setup @{binding safe_step} (cla_method' safe_step_tac)
+    "single classical step (safe rules)" #>
+  Method.setup @{binding inst_step} (cla_method' inst_step_tac)
+    "single classical step (safe rules, allow instantiations)" #>
+  Method.setup @{binding step} (cla_method' step_tac)
+    "single classical step (safe and unsafe rules)" #>
+  Method.setup @{binding slow_step} (cla_method' slow_step_tac)
+    "single classical step (safe and unsafe rules, allow backtracking)" #>
+  Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
+    "single classical step (safe rules, without splitting)";