52 isar_shrink_factor, ...} : params) silent (prover : prover) |
52 isar_shrink_factor, ...} : params) silent (prover : prover) |
53 explicit_apply timeout i n state facts = |
53 explicit_apply timeout i n state facts = |
54 let |
54 let |
55 val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...") |
55 val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...") |
56 val params = |
56 val params = |
57 {blocking = true, debug = debug, verbose = false, overlord = overlord, |
57 {debug = debug, verbose = false, overlord = overlord, blocking = true, |
58 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
58 provers = provers, type_sys = type_sys, explicit_apply = explicit_apply, |
59 relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
59 relevance_thresholds = (1.01, 1.01), max_relevant = NONE, |
60 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
60 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
61 timeout = timeout, expect = ""} |
61 timeout = timeout, expect = ""} |
62 val facts = |
62 val facts = |