equal
deleted
inserted
replaced
230 [Pretty.block |
230 [Pretty.block |
231 (Pretty.breaks |
231 (Pretty.breaks |
232 (Pretty.str "(co)inductives:" :: |
232 (Pretty.str "(co)inductives:" :: |
233 map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))), |
233 map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))), |
234 Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)] |
234 Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)] |
235 end |> Pretty.chunks |> Pretty.writeln; |
235 end |> Pretty.writeln_chunks; |
236 |
236 |
237 |
237 |
238 (* inductive info *) |
238 (* inductive info *) |
239 |
239 |
240 fun the_inductive ctxt name = |
240 fun the_inductive ctxt name = |