exported read|cert_arity interfaces
authorhaftmann
Wed Jan 04 17:03:43 2006 +0100 (2006-01-04 ago)
changeset 1857446ed84a64cf6
parent 18573 0ee7eab8c845
child 18575 9ccfd1d1e874
exported read|cert_arity interfaces
src/Pure/axclass.ML
     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;