--- 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 *)