113 Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
113 Int.min (msecs, Time.toMilliseconds time + fudge_msecs) |
114 |> Time.fromMilliseconds |
114 |> Time.fromMilliseconds |
115 val (min_thms, {proof, internal_thm_names, ...}) = |
115 val (min_thms, {proof, internal_thm_names, ...}) = |
116 sublinear_minimize (test_facts new_timeout) |
116 sublinear_minimize (test_facts new_timeout) |
117 (filter_used_facts used_thm_names name_thms_pairs) ([], result) |
117 (filter_used_facts used_thm_names name_thms_pairs) ([], result) |
118 val m = length min_thms |
118 val n = length min_thms |
119 val _ = priority (cat_lines |
119 val _ = priority (cat_lines |
120 ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".") |
120 ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ |
|
121 (case filter (String.isPrefix chained_prefix o fst) min_thms of |
|
122 [] => "" |
|
123 | chained => " (including " ^ Int.toString (length chained) ^ |
|
124 " chained)") ^ ".") |
121 in |
125 in |
122 (SOME min_thms, |
126 (SOME min_thms, |
123 proof_text isar_proof |
127 proof_text isar_proof |
124 (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
128 (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) |
125 (full_types, K "", proof, internal_thm_names, goal, i) |> fst) |
129 (full_types, K "", proof, internal_thm_names, goal, i) |> fst) |