equal
deleted
inserted
replaced
239 |
239 |
240 val is_registered = is_some oo lookup_pred_data o ProofContext.theory_of |
240 val is_registered = is_some oo lookup_pred_data o ProofContext.theory_of |
241 |
241 |
242 val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of |
242 val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of |
243 |
243 |
244 fun intros_of thy = map (Thm.transfer thy) o #intros o the_pred_data thy |
244 fun intros_of thy = #intros o the_pred_data thy |
245 |
245 |
246 fun the_elim_of thy name = case #elim (the_pred_data thy name) |
246 fun the_elim_of thy name = case #elim (the_pred_data thy name) |
247 of NONE => error ("No elimination rule for predicate " ^ quote name) |
247 of NONE => error ("No elimination rule for predicate " ^ quote name) |
248 | SOME thm => Thm.transfer thy thm |
248 | SOME thm => Thm.transfer thy thm |
249 |
249 |