diff -r cd3a09c7dac9 -r 704e50ab65af src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Dec 05 03:07:44 2001 +0100
+++ b/src/Pure/drule.ML	Wed Dec 05 03:09:21 2001 +0100
@@ -101,6 +101,8 @@
   val close_derivation: thm -> thm
   val local_standard: thm -> thm
   val compose_single: thm * int * thm -> thm
+  val add_rule: thm -> thm list -> thm list
+  val del_rule: thm -> thm list -> thm list
   val add_rules: thm list -> thm list -> thm list
   val del_rules: thm list -> thm list -> thm list
   val merge_rules: thm list * thm list -> thm list
@@ -490,6 +492,8 @@
 (*maintain lists of theorems --- preserving canonical order*)
 fun del_rules rs rules = Library.gen_rems Thm.eq_thm (rules, rs);
 fun add_rules rs rules = rs @ del_rules rs rules;
+val del_rule = del_rules o single;
+val add_rule = add_rules o single;
 fun merge_rules (rules1, rules2) = gen_merge_lists' Thm.eq_thm rules1 rules2;