exported read|cert_arity interfaces
authorhaftmann
Wed, 04 Jan 2006 17:03:43 +0100
changeset 18574 46ed84a64cf6
parent 18573 0ee7eab8c845
child 18575 9ccfd1d1e874
exported read|cert_arity interfaces
src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Jan 04 16:38:40 2006 +0100
+++ b/src/Pure/axclass.ML	Wed Jan 04 17:03:43 2006 +0100
@@ -24,6 +24,8 @@
   val instance_subclass_i: class * class -> theory -> Proof.state
   val instance_arity: xstring * string list * string -> theory -> Proof.state
   val instance_arity_i: string * sort list * sort -> theory -> Proof.state
+  val read_arity: theory -> xstring * string list * string -> arity
+  val cert_arity: theory -> string * sort list * sort -> arity
   val intro_classes_tac: thm list -> tactic
   val default_intro_classes_tac: thm list -> tactic
 end;