tuned signature;
authorwenzelm
Tue Apr 27 19:44:04 2010 +0200 (2010-04-27 ago)
changeset 3642785bc9b7c4d18
parent 36426 cc8db7295249
child 36428 874843c1e96e
tuned signature;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 27 16:24:57 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 27 19:44:04 2010 +0200
     1.3 @@ -7,35 +7,35 @@
     1.4  
     1.5  signature AX_CLASS =
     1.6  sig
     1.7 -  val define_class: binding * class list -> string list ->
     1.8 -    (Thm.binding * term list) list -> theory -> class * theory
     1.9 +  type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
    1.10 +  val get_info: theory -> class -> info
    1.11 +  val class_of_param: theory -> string -> class option
    1.12 +  val instance_name: string * class -> string
    1.13 +  val thynames_of_arity: theory -> class * string -> string list
    1.14 +  val param_of_inst: theory -> string * string -> string
    1.15 +  val inst_of_param: theory -> string -> (string * string) option
    1.16 +  val unoverload: theory -> thm -> thm
    1.17 +  val overload: theory -> thm -> thm
    1.18 +  val unoverload_conv: theory -> conv
    1.19 +  val overload_conv: theory -> conv
    1.20 +  val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
    1.21 +  val unoverload_const: theory -> string * typ -> string
    1.22 +  val cert_classrel: theory -> class * class -> class * class
    1.23 +  val read_classrel: theory -> xstring * xstring -> class * class
    1.24 +  val declare_overloaded: string * typ -> theory -> term * theory
    1.25 +  val define_overloaded: binding -> string * term -> theory -> thm * theory
    1.26    val add_classrel: thm -> theory -> theory
    1.27    val add_arity: thm -> theory -> theory
    1.28    val prove_classrel: class * class -> tactic -> theory -> theory
    1.29    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
    1.30 -  type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
    1.31 -  val get_info: theory -> class -> info
    1.32 -  val class_of_param: theory -> string -> class option
    1.33 -  val cert_classrel: theory -> class * class -> class * class
    1.34 -  val read_classrel: theory -> xstring * xstring -> class * class
    1.35 +  val define_class: binding * class list -> string list ->
    1.36 +    (Thm.binding * term list) list -> theory -> class * theory
    1.37    val axiomatize_class: binding * class list -> theory -> theory
    1.38    val axiomatize_class_cmd: binding * xstring list -> theory -> theory
    1.39    val axiomatize_classrel: (class * class) list -> theory -> theory
    1.40    val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
    1.41    val axiomatize_arity: arity -> theory -> theory
    1.42    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
    1.43 -  val instance_name: string * class -> string
    1.44 -  val declare_overloaded: string * typ -> theory -> term * theory
    1.45 -  val define_overloaded: binding -> string * term -> theory -> thm * theory
    1.46 -  val unoverload: theory -> thm -> thm
    1.47 -  val overload: theory -> thm -> thm
    1.48 -  val unoverload_conv: theory -> conv
    1.49 -  val overload_conv: theory -> conv
    1.50 -  val unoverload_const: theory -> string * typ -> string
    1.51 -  val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
    1.52 -  val param_of_inst: theory -> string * string -> string
    1.53 -  val inst_of_param: theory -> string -> (string * string) option
    1.54 -  val thynames_of_arity: theory -> class * string -> string list
    1.55  end;
    1.56  
    1.57  structure AxClass: AX_CLASS =