equal
deleted
inserted
replaced
211 |
211 |
212 fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs); |
212 fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs); |
213 |
213 |
214 fun pretty_rules ctxt kind rs = |
214 fun pretty_rules ctxt kind rs = |
215 let val thms = map snd (Item_Net.content rs) |
215 let val thms = map snd (Item_Net.content rs) |
216 in Pretty.big_list kind (map (Pretty.item o single o Display.pretty_thm ctxt) thms) end; |
216 in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end; |
217 |
217 |
218 |
218 |
219 (* context data *) |
219 (* context data *) |
220 |
220 |
221 structure Data = Generic_Data |
221 structure Data = Generic_Data |