equal
deleted
inserted
replaced
460 end; |
460 end; |
461 |
461 |
462 in |
462 in |
463 |
463 |
464 fun pretty_thm ctxt (thmref, thm) = |
464 fun pretty_thm ctxt (thmref, thm) = |
465 Pretty.block (pretty_ref ctxt thmref @ [Display.pretty_thm ctxt thm]); |
465 Pretty.block (pretty_ref ctxt thmref @ [Thm.pretty_thm ctxt thm]); |
466 |
466 |
467 fun pretty_theorems state opt_limit rem_dups raw_criteria = |
467 fun pretty_theorems state opt_limit rem_dups raw_criteria = |
468 let |
468 let |
469 val ctxt = Proof.context_of state; |
469 val ctxt = Proof.context_of state; |
470 val opt_goal = try Proof.simple_goal state |> Option.map #goal; |
470 val opt_goal = try Proof.simple_goal state |> Option.map #goal; |