Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/CASC_Setup.thy
changeset 43205 23b81469499f
parent 43161 27dcda8fc89b
child 43211 77c432fe28ff
equal deleted inserted replaced
43204:ac02112a208e 43205:23b81469499f 
    49    SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
 
    49    SOLVE_TIMEOUT (max_secs div 20) "blast" (ALLGOALS (blast_tac ctxt))
 
    50    ORELSE
 
    50    ORELSE
 
    51    SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
 
    51    SOLVE_TIMEOUT (max_secs div 10) "auto" (auto_tac ctxt
 
    52        THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
 
    52        THEN ALLGOALS (Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt))
 
    53    ORELSE
 
    53    ORELSE
 
    54    SOLVE_TIMEOUT (max_secs div 10) "metis" (ALLGOALS (Metis_Tactics.metis_tac ctxt []))
 
    54    SOLVE_TIMEOUT (max_secs div 10) "metis"
 
       
    55        (ALLGOALS (Metis_Tactics.new_metis_tac ctxt NONE []))
 
    55    ORELSE
 
    56    ORELSE
 
    56    SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
 
    57    SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt))
 
    57    ORELSE
 
    58    ORELSE
 
    58    SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
 
    59    SOLVE_TIMEOUT (max_secs div 10) "best" (ALLGOALS (best_tac ctxt))
 
    59    ORELSE
 
    60    ORELSE
isabelle