equal
deleted
inserted
replaced
47 val check: theory -> xstring * Position.T -> string |
47 val check: theory -> xstring * Position.T -> string |
48 val extern: theory -> string -> xstring |
48 val extern: theory -> string -> xstring |
49 val markup_name: Proof.context -> string -> string |
49 val markup_name: Proof.context -> string -> string |
50 val pretty_name: Proof.context -> string -> Pretty.T |
50 val pretty_name: Proof.context -> string -> Pretty.T |
51 val defined: theory -> string -> bool |
51 val defined: theory -> string -> bool |
|
52 val parameters_of: theory -> string -> (string * sort) list * ((string * typ) * mixfix) list |
52 val params_of: theory -> string -> ((string * typ) * mixfix) list |
53 val params_of: theory -> string -> ((string * typ) * mixfix) list |
53 val intros_of: theory -> string -> thm option * thm option |
54 val intros_of: theory -> string -> thm option * thm option |
54 val axioms_of: theory -> string -> thm list |
55 val axioms_of: theory -> string -> thm list |
55 val instance_of: theory -> string -> morphism -> term list |
56 val instance_of: theory -> string -> morphism -> term list |
56 val specification_of: theory -> string -> term option * term list |
57 val specification_of: theory -> string -> term option * term list |
220 |
221 |
221 |
222 |
222 |
223 |
223 (** Primitive operations **) |
224 (** Primitive operations **) |
224 |
225 |
225 fun params_of thy = snd o #parameters o the_locale thy; |
226 fun parameters_of thy = #parameters o the_locale thy; |
|
227 val params_of = #2 oo parameters_of; |
226 |
228 |
227 fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy; |
229 fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy; |
228 |
230 |
229 fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy; |
231 fun axioms_of thy = map (Thm.transfer thy) o #axioms o the_locale thy; |
230 |
232 |