export name_multi;
authorwenzelm
Wed, 25 Jan 2006 00:21:36 +0100
changeset 18778 f623f7a35ced
parent 18777 9d98d5705433
child 18779 a9f41c380b2f
export name_multi;
src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Jan 25 00:21:35 2006 +0100
+++ b/src/Pure/pure_thy.ML	Wed Jan 25 00:21:36 2006 +0100
@@ -52,6 +52,7 @@
   val smart_store_thms_open: (bstring * thm list) -> thm list
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
+  val name_multi: string -> 'a list -> (string * 'a) list
   val add_thms: ((bstring * thm) * attribute list) list -> theory -> thm list * theory
   val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory 
   val note_thmss: attribute -> ((bstring * attribute list) *