equal
deleted
inserted
replaced
92 val class_deps: Toplevel.transition -> Toplevel.transition |
92 val class_deps: Toplevel.transition -> Toplevel.transition |
93 val thy_deps: Toplevel.transition -> Toplevel.transition |
93 val thy_deps: Toplevel.transition -> Toplevel.transition |
94 val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition |
94 val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition |
95 val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list |
95 val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list |
96 -> Toplevel.transition -> Toplevel.transition |
96 -> Toplevel.transition -> Toplevel.transition |
|
97 val unused_thms: (string list * string list option) option -> |
|
98 Toplevel.transition -> Toplevel.transition |
97 val print_binds: Toplevel.transition -> Toplevel.transition |
99 val print_binds: Toplevel.transition -> Toplevel.transition |
98 val print_cases: Toplevel.transition -> Toplevel.transition |
100 val print_cases: Toplevel.transition -> Toplevel.transition |
99 val print_stmts: string list * (thmref * Attrib.src list) list |
101 val print_stmts: string list * (thmref * Attrib.src list) list |
100 -> Toplevel.transition -> Toplevel.transition |
102 -> Toplevel.transition -> Toplevel.transition |
101 val print_thms: string list * (thmref * Attrib.src list) list |
103 val print_thms: string list * (thmref * Attrib.src list) list |
529 val ctxt = Proof.context_of proof_state; |
531 val ctxt = Proof.context_of proof_state; |
530 val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2); |
532 val opt_goal = try Proof.get_goal proof_state |> Option.map (Thm.prop_of o #2 o #2); |
531 in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end); |
533 in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end); |
532 |
534 |
533 |
535 |
|
536 (* find unused theorems *) |
|
537 |
|
538 local |
|
539 |
|
540 fun pretty_name_thm (a, th) = |
|
541 Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, Display.pretty_thm th]; |
|
542 |
|
543 in |
|
544 |
|
545 fun unused_thms opt_range = |
|
546 Toplevel.keep (fn state => ThmDeps.unused_thms |
|
547 (case opt_range of |
|
548 NONE => (NONE, [Toplevel.theory_of state]) |
|
549 | SOME (xs, NONE) => |
|
550 (SOME (map ThyInfo.get_theory xs), [Toplevel.theory_of state]) |
|
551 | SOME (xs, SOME ys) => |
|
552 (SOME (map ThyInfo.get_theory xs), map ThyInfo.get_theory ys)) |> |
|
553 map pretty_name_thm |> Pretty.chunks |> Pretty.writeln); |
|
554 |
|
555 end; |
|
556 |
|
557 |
534 (* print proof context contents *) |
558 (* print proof context contents *) |
535 |
559 |
536 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => |
560 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => |
537 ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); |
561 ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); |
538 |
562 |