src/Provers/classical.ML
changeset 50108 f171b5240c31
parent 50062 e038198f7d08
child 50112 11cd86c5af3a
     1.1 --- a/src/Provers/classical.ML	Sat Nov 17 17:55:52 2012 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Nov 17 19:46:32 2012 +0100
     1.3 @@ -948,7 +948,17 @@
     1.4        >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
     1.5      "classical prover (iterative deepening)" #>
     1.6    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
     1.7 -    "classical prover (apply safe rules)";
     1.8 +    "classical prover (apply safe rules)" #>
     1.9 +  Method.setup @{binding safe_step} (cla_method' safe_step_tac)
    1.10 +    "single classical step (safe rules)" #>
    1.11 +  Method.setup @{binding inst_step} (cla_method' inst_step_tac)
    1.12 +    "single classical step (safe rules, allow instantiations)" #>
    1.13 +  Method.setup @{binding step} (cla_method' step_tac)
    1.14 +    "single classical step (safe and unsafe rules)" #>
    1.15 +  Method.setup @{binding slow_step} (cla_method' slow_step_tac)
    1.16 +    "single classical step (safe and unsafe rules, allow backtracking)" #>
    1.17 +  Method.setup @{binding clarify_step} (cla_method' clarify_step_tac)
    1.18 +    "single classical step (safe rules, without splitting)";
    1.19  
    1.20  
    1.21