src/Pure/Tools/named_theorems.ML
changeset 61900 3f5e2e0a6d29
parent 61049 0d401f874942
child 62848 e4140efe699e
     1.1 --- a/src/Pure/Tools/named_theorems.ML	Tue Dec 22 10:35:35 2015 +0100
     1.2 +++ b/src/Pure/Tools/named_theorems.ML	Tue Dec 22 10:58:05 2015 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    val member: Proof.context -> string -> thm -> bool
     1.6    val get: Proof.context -> string -> thm list
     1.7 +  val clear: string -> Context.generic -> Context.generic
     1.8    val add_thm: string -> thm -> Context.generic -> Context.generic
     1.9    val del_thm: string -> thm -> Context.generic -> Context.generic
    1.10    val add: string -> attribute
    1.11 @@ -55,6 +56,8 @@
    1.12  
    1.13  val get = content o Context.Proof;
    1.14  
    1.15 +fun clear name = map_entry name (K Thm.full_rules);
    1.16 +
    1.17  fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
    1.18  fun del_thm name = map_entry name o Item_Net.remove;
    1.19