tuned signature;
authorwenzelm
Thu, 02 Apr 2009 14:49:50 +0200
changeset 30853 6c6b7a72fa34
parent 30852 59a422908e29
child 30854 740517878d60
tuned signature;
src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Apr 02 14:30:16 2009 +0200
+++ b/src/Pure/pure_thy.ML	Thu Apr 02 14:49:50 2009 +0200
@@ -31,10 +31,10 @@
   val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
-  val note_thmss: string -> (Thm.binding *
-      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
-  val note_thmss_grouped: string -> string -> (Thm.binding *
-      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
+    -> theory -> (string * thm list) list * theory
+  val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
+    -> theory -> (string * thm list) list * theory
   val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->