equal
deleted
inserted
replaced
406 in find (all_facts_of ctxt) end; |
406 in find (all_facts_of ctxt) end; |
407 |
407 |
408 |
408 |
409 fun pretty_thm ctxt (thmref, thm) = Pretty.block |
409 fun pretty_thm ctxt (thmref, thm) = Pretty.block |
410 [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, |
410 [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1, |
411 ProofContext.pretty_thm ctxt thm]; |
411 Display.pretty_thm ctxt thm]; |
412 |
412 |
413 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = |
413 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = |
414 let |
414 let |
415 val start = start_timing (); |
415 val start = start_timing (); |
416 |
416 |