equal
deleted
inserted
replaced
85 val prep_ext = mk_empty; |
85 val prep_ext = mk_empty; |
86 val merge = mk_empty; |
86 val merge = mk_empty; |
87 |
87 |
88 fun pretty sg (ref {space, thms_tab, const_idx = _}) = |
88 fun pretty sg (ref {space, thms_tab, const_idx = _}) = |
89 let |
89 let |
90 val prt_thm = Display.pretty_thm o Thm.transfer_sg sg; |
90 val prt_thm = Display.pretty_thm_sg sg; |
91 fun prt_thms (name, [th]) = |
91 fun prt_thms (name, [th]) = |
92 Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th] |
92 Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th] |
93 | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths); |
93 | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths); |
94 |
94 |
95 val thmss = NameSpace.cond_extern_table space thms_tab; |
95 val thmss = NameSpace.cond_extern_table space thms_tab; |
211 |
211 |
212 (*search globally*) |
212 (*search globally*) |
213 fun thms_containing thy consts = |
213 fun thms_containing thy consts = |
214 (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of |
214 (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of |
215 [] => flat (map (containing consts) (thy :: Theory.ancestors_of thy)) |
215 [] => flat (map (containing consts) (thy :: Theory.ancestors_of thy)) |
216 | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy])); |
216 | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy])) |
|
217 |> map (apsnd (Thm.transfer thy)); |
217 |
218 |
218 |
219 |
219 |
220 |
220 (** store theorems **) (*DESTRUCTIVE*) |
221 (** store theorems **) (*DESTRUCTIVE*) |
221 |
222 |