src/Pure/Isar/locale.ML
changeset 67694 ab68ca1e80ba
parent 67680 175a070e9dd8
child 67714 a0b58be402ab
equal deleted inserted replaced
67682:00c436488398 67694:ab68ca1e80ba
    47   val extern: theory -> string -> xstring
    47   val extern: theory -> string -> xstring
    48   val markup_name: Proof.context -> string -> string
    48   val markup_name: Proof.context -> string -> string
    49   val pretty_name: Proof.context -> string -> Pretty.T
    49   val pretty_name: Proof.context -> string -> Pretty.T
    50   val defined: theory -> string -> bool
    50   val defined: theory -> string -> bool
    51   val params_of: theory -> string -> ((string * typ) * mixfix) list
    51   val params_of: theory -> string -> ((string * typ) * mixfix) list
       
    52   val params_types_of: theory -> string -> string list * typ list
    52   val intros_of: theory -> string -> thm option * thm option
    53   val intros_of: theory -> string -> thm option * thm option
    53   val axioms_of: theory -> string -> thm list
    54   val axioms_of: theory -> string -> thm list
    54   val instance_of: theory -> string -> morphism -> term list
    55   val instance_of: theory -> string -> morphism -> term list
    55   val specification_of: theory -> string -> term option * term list
    56   val specification_of: theory -> string -> term option * term list
    56 
    57 
   210 
   211 
   211 
   212 
   212 (** Primitive operations **)
   213 (** Primitive operations **)
   213 
   214 
   214 fun params_of thy = snd o #parameters o the_locale thy;
   215 fun params_of thy = snd o #parameters o the_locale thy;
       
   216 fun params_types_of thy loc = split_list (map #1 (params_of thy loc));
   215 
   217 
   216 fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy;
   218 fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy;
   217 
   219 
   218 fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy;
   220 fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy;
   219 
   221