src/HOL/Tools/Sledgehammer/named_thm_set.ML
changeset 36314 cf1abb4daae6
parent 36313 f2753d6b0859
parent 36297 6b2b9516a3cd
child 36315 e859879079c8
     1.1 --- a/src/HOL/Tools/Sledgehammer/named_thm_set.ML	Fri Apr 23 19:32:37 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,45 +0,0 @@
     1.4 -(*  Title:      HOL/Tools/Sledgehammer/named_thm_set.ML
     1.5 -    Author:     Makarius
     1.6 -    Author:     Jasmin Blanchette, TU Muenchen
     1.7 -
     1.8 -Named sets of theorems.
     1.9 -*)
    1.10 -
    1.11 -signature NAMED_THM_SET =
    1.12 -sig
    1.13 -  val member: Proof.context -> thm -> bool
    1.14 -  val add_thm: thm -> Context.generic -> Context.generic
    1.15 -  val del_thm: thm -> Context.generic -> Context.generic
    1.16 -  val add: attribute
    1.17 -  val del: attribute
    1.18 -  val setup: theory -> theory
    1.19 -end;
    1.20 -
    1.21 -functor Named_Thm_Set(val name: string val description: string)
    1.22 -        : NAMED_THM_SET =
    1.23 -struct
    1.24 -
    1.25 -structure Data = Generic_Data
    1.26 -(
    1.27 -  type T = thm Termtab.table;
    1.28 -  val empty = Termtab.empty;
    1.29 -  val extend = I;
    1.30 -  fun merge tabs = Termtab.merge (K true) tabs;
    1.31 -);
    1.32 -
    1.33 -fun member ctxt th =
    1.34 -  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
    1.35 -
    1.36 -fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
    1.37 -fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
    1.38 -
    1.39 -val add = Thm.declaration_attribute add_thm;
    1.40 -val del = Thm.declaration_attribute del_thm;
    1.41 -
    1.42 -val setup =
    1.43 -  Attrib.setup (Binding.name name) (Attrib.add_del add del)
    1.44 -               ("declaration of " ^ description) #>
    1.45 -  PureThy.add_thms_dynamic (Binding.name name,
    1.46 -                            map #2 o Termtab.dest o Data.get);
    1.47 -
    1.48 -end;