equal
deleted
inserted
replaced
190 end |
190 end |
191 |
191 |
192 val auto_try_max_facts_divisor = 2 (* FUDGE *) |
192 val auto_try_max_facts_divisor = 2 (* FUDGE *) |
193 |
193 |
194 fun string_of_facts facts = |
194 fun string_of_facts facts = |
195 "Including " ^ string_of_int (length facts) ^ |
195 "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ |
196 " relevant fact" ^ plural_s (length facts) ^ ":\n" ^ |
|
197 (facts |> map (fst o fst) |> space_implode " ") ^ "." |
196 (facts |> map (fst o fst) |> space_implode " ") ^ "." |
198 |
197 |
199 fun string_of_factss factss = |
198 fun string_of_factss factss = |
200 if forall (null o snd) factss then |
199 if forall (null o snd) factss then |
201 "Found no relevant facts." |
200 "Found no relevant facts." |