src/Tools/solve_direct.ML
changeset 58842 22b87ab47d3b
parent 56467 8d7d6f17c6a7
child 58843 521cea5fa777
equal deleted inserted replaced
58840:f4bb3068d819 58842:22b87ab47d3b
    31 
    31 
    32 
    32 
    33 (* preferences *)
    33 (* preferences *)
    34 
    34 
    35 val max_solutions = Unsynchronized.ref 5;
    35 val max_solutions = Unsynchronized.ref 5;
    36 
       
    37 val _ =
       
    38   ProofGeneral.preference_option ProofGeneral.category_tracing
       
    39     NONE
       
    40     @{system_option auto_solve_direct}
       
    41     "auto-solve-direct"
       
    42     ("Run " ^ quote solve_directN ^ " automatically");
       
    43 
    36 
    44 
    37 
    45 (* solve_direct command *)
    38 (* solve_direct command *)
    46 
    39 
    47 fun do_solve_direct mode state =
    40 fun do_solve_direct mode state =