equal
deleted
inserted
replaced
149 fun print_inductives ctxt = |
149 fun print_inductives ctxt = |
150 let |
150 let |
151 val (tab, monos) = get_inductives ctxt; |
151 val (tab, monos) = get_inductives ctxt; |
152 val space = Consts.space_of (ProofContext.consts_of ctxt); |
152 val space = Consts.space_of (ProofContext.consts_of ctxt); |
153 in |
153 in |
154 [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))), |
154 [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))), |
155 Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] |
155 Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)] |
156 |> Pretty.chunks |> Pretty.writeln |
156 |> Pretty.chunks |> Pretty.writeln |
157 end; |
157 end; |
158 |
158 |
159 |
159 |