equal
deleted
inserted
replaced
62 val class_deps: Toplevel.transition -> Toplevel.transition |
62 val class_deps: Toplevel.transition -> Toplevel.transition |
63 val thy_deps: Toplevel.transition -> Toplevel.transition |
63 val thy_deps: Toplevel.transition -> Toplevel.transition |
64 val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition |
64 val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition |
65 val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list |
65 val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list |
66 -> Toplevel.transition -> Toplevel.transition |
66 -> Toplevel.transition -> Toplevel.transition |
|
67 val find_consts: (bool * FindConsts.criterion) list -> |
|
68 Toplevel.transition -> Toplevel.transition |
67 val unused_thms: (string list * string list option) option -> |
69 val unused_thms: (string list * string list option) option -> |
68 Toplevel.transition -> Toplevel.transition |
70 Toplevel.transition -> Toplevel.transition |
69 val print_binds: Toplevel.transition -> Toplevel.transition |
71 val print_binds: Toplevel.transition -> Toplevel.transition |
70 val print_cases: Toplevel.transition -> Toplevel.transition |
72 val print_cases: Toplevel.transition -> Toplevel.transition |
71 val print_stmts: string list * (Facts.ref * Attrib.src list) list |
73 val print_stmts: string list * (Facts.ref * Attrib.src list) list |
430 | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy]) |
432 | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy]) |
431 | SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys)) |
433 | SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys)) |
432 |> map pretty_thm |> Pretty.chunks |> Pretty.writeln |
434 |> map pretty_thm |> Pretty.chunks |> Pretty.writeln |
433 end); |
435 end); |
434 |
436 |
|
437 (* retrieve constants *) |
|
438 |
|
439 fun find_consts spec = |
|
440 Toplevel.unknown_theory o Toplevel.keep (fn state => |
|
441 let val ctxt = (Proof.context_of o Toplevel.enter_proof_body) state |
|
442 in FindConsts.find_consts ctxt spec end); |
435 |
443 |
436 (* print proof context contents *) |
444 (* print proof context contents *) |
437 |
445 |
438 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => |
446 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state => |
439 ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); |
447 ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state)); |