src/Pure/axclass.ML
changeset 18574 46ed84a64cf6
parent 18467 bb7b309ac395
child 18678 dd0c569fa43d
     1.1 --- a/src/Pure/axclass.ML	Wed Jan 04 16:38:40 2006 +0100
     1.2 +++ b/src/Pure/axclass.ML	Wed Jan 04 17:03:43 2006 +0100
     1.3 @@ -24,6 +24,8 @@
     1.4    val instance_subclass_i: class * class -> theory -> Proof.state
     1.5    val instance_arity: xstring * string list * string -> theory -> Proof.state
     1.6    val instance_arity_i: string * sort list * sort -> theory -> Proof.state
     1.7 +  val read_arity: theory -> xstring * string list * string -> arity
     1.8 +  val cert_arity: theory -> string * sort list * sort -> arity
     1.9    val intro_classes_tac: thm list -> tactic
    1.10    val default_intro_classes_tac: thm list -> tactic
    1.11  end;