Made local_note_prefix public.
authorballarin
Fri Nov 14 14:00:52 2008 +0100 (2008-11-14)
changeset 287944493633ab401
parent 28793 bb7a102e2f5d
child 28795 6891e273c33b
Made local_note_prefix public.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Nov 14 08:50:11 2008 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Fri Nov 14 14:00:52 2008 +0100
     1.3 @@ -91,6 +91,9 @@
     1.4    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
     1.5  
     1.6    (* Storing results *)
     1.7 +  val local_note_prefix: string ->
     1.8 +    (Name.binding * attribute list) * (thm list * attribute list) list ->
     1.9 +    Proof.context -> (string * thm list) * Proof.context
    1.10    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
    1.11      Proof.context -> Proof.context
    1.12    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context