src/HOL/Tools/recdef_package.ML
changeset 10268 ca52783f9801
parent 10032 1823b34834fd
child 10775 3a5e5657e41c
equal deleted inserted replaced
10267:325ead6d9457 10268:ca52783f9801
    10 sig
    10 sig
    11   val quiet_mode: bool ref
    11   val quiet_mode: bool ref
    12   val print_recdefs: theory -> unit
    12   val print_recdefs: theory -> unit
    13   val get_recdef: theory -> string
    13   val get_recdef: theory -> string
    14     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
    14     -> {simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
       
    15   val tcs_of: theory -> xstring -> term list
    15   val simp_add_global: theory attribute
    16   val simp_add_global: theory attribute
    16   val simp_del_global: theory attribute
    17   val simp_del_global: theory attribute
    17   val cong_add_global: theory attribute
    18   val cong_add_global: theory attribute
    18   val cong_del_global: theory attribute
    19   val cong_del_global: theory attribute
    19   val wf_add_global: theory attribute
    20   val wf_add_global: theory attribute
   136 
   137 
   137 val get_global_hints = #2 o GlobalRecdefData.get;
   138 val get_global_hints = #2 o GlobalRecdefData.get;
   138 val map_global_hints = GlobalRecdefData.map o apsnd;
   139 val map_global_hints = GlobalRecdefData.map o apsnd;
   139 
   140 
   140 
   141 
       
   142 fun tcs_of thy raw_name =
       
   143   let val name = Sign.intern_const (Theory.sign_of thy) raw_name in
       
   144     (case get_recdef thy name of
       
   145       None => error ("No recdef definition of constant: " ^ quote name)
       
   146     | Some {tcs, ...} => tcs)
       
   147   end;
       
   148 
       
   149 
   141 (* proof data kind 'HOL/recdef' *)
   150 (* proof data kind 'HOL/recdef' *)
   142 
   151 
   143 structure LocalRecdefArgs =
   152 structure LocalRecdefArgs =
   144 struct
   153 struct
   145   val name = "HOL/recdef";
   154   val name = "HOL/recdef";