src/Provers/classical.ML
changeset 42798 02c88bdabe75
parent 42793 88bee9f6eec7
child 42799 4e33894aec6d
     1.1 --- a/src/Provers/classical.ML	Fri May 13 23:59:48 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat May 14 00:32:16 2011 +0200
     1.3 @@ -942,7 +942,9 @@
     1.4    Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
     1.5    Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
     1.6    Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
     1.7 -  Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
     1.8 +  Method.setup @{binding deepen}
     1.9 +    (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
    1.10 +      >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
    1.11      "classical prover (iterative deepening)" #>
    1.12    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
    1.13      "classical prover (apply safe rules)";