equal
deleted
inserted
replaced
118 fun prt_kind (i, b) = |
118 fun prt_kind (i, b) = |
119 Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") |
119 Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":") |
120 (map_filter (fn (_, (k, th)) => |
120 (map_filter (fn (_, (k, th)) => |
121 if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE) |
121 if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE) |
122 (sort (int_ord o pairself fst) rules)); |
122 (sort (int_ord o pairself fst) rules)); |
123 in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end; |
123 in Pretty.writeln_chunks (map prt_kind rule_kinds) end; |
124 |
124 |
125 |
125 |
126 (* access data *) |
126 (* access data *) |
127 |
127 |
128 fun netpairs ctxt = let val Rules {netpairs, ...} = Rules.get (Context.Proof ctxt) in netpairs end; |
128 fun netpairs ctxt = let val Rules {netpairs, ...} = Rules.get (Context.Proof ctxt) in netpairs end; |