# HG changeset patch
# User haftmann
# Date 1174913586 -7200
# Node ID 19e4fd6ffcaa197f3907f9dbdeafd28653ed0766
# Parent  783c8dbe3ade2db54ad9db8381692e6678695dfa
exported interface for intro rules

diff -r 783c8dbe3ade -r 19e4fd6ffcaa src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Mar 26 14:53:05 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Mar 26 14:53:06 2007 +0200
@@ -49,7 +49,6 @@
   val init: string -> theory -> Proof.context
 
   (* The specification of a locale *)
-
   val parameters_of: theory -> string ->
     ((string * typ) * mixfix) list
   val parameters_of_expr: theory -> expr ->
@@ -58,6 +57,8 @@
     ((string * Attrib.src list) * term list) list
   val global_asms_of: theory -> string ->
     ((string * Attrib.src list) * term list) list
+  val intros: theory -> string ->
+    thm list * thm list
 
   (* Processing of locale statements *)
   val read_context_statement: xstring option -> Element.context element list ->
@@ -1374,6 +1375,11 @@
 
 end;
 
+fun intros thy =
+  #intros o the o Symtab.lookup (#2 (GlobalLocalesData.get thy));
+    (*returns introduction rule for delta predicate and locale predicate
+      as a pair of singleton lists*)
+
 
 (* full context statements: import + elements + conclusion *)