equal
deleted
inserted
replaced
481 "found " ^ string_of_int found ^ " theorem(s)" ^ |
481 "found " ^ string_of_int found ^ " theorem(s)" ^ |
482 (if returned < found |
482 (if returned < found |
483 then " (" ^ string_of_int returned ^ " displayed)" |
483 then " (" ^ string_of_int returned ^ " displayed)" |
484 else "")); |
484 else "")); |
485 in |
485 in |
486 Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: |
486 Pretty.block |
|
487 (Pretty.keyword1 "find_theorems" :: Pretty.brk 1 :: Pretty.str "query:" :: Pretty.fbrk :: |
|
488 Pretty.fbreaks (map (pretty_criterion ctxt) criteria)) :: |
487 Pretty.str "" :: |
489 Pretty.str "" :: |
488 (if null theorems then [Pretty.str "nothing found"] |
490 (if null theorems then [Pretty.str "nothing found"] |
489 else |
491 else |
490 [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ |
492 [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @ |
491 grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems)) |
493 grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems)) |