--- a/src/Pure/pure_thy.ML Tue Jan 12 15:17:37 1999 +0100
+++ b/src/Pure/pure_thy.ML Tue Jan 12 15:18:47 1999 +0100
@@ -11,6 +11,7 @@
val print_theory: theory -> unit
val get_thm: theory -> xstring -> thm
val get_thms: theory -> xstring -> thm list
+ val get_thmss: theory -> xstring list -> thm list
val thms_of: theory -> (string * thm) list
structure ProtoPure:
sig
@@ -24,7 +25,6 @@
sig
include BASIC_PURE_THY
val thms_closure: theory -> xstring -> thm list option
- val get_thmss: theory -> xstring list -> thm list
val thms_containing: theory -> string list -> (string * thm) list
val default_name: string -> string
val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm