# HG changeset patch
# User wenzelm
# Date 1114538125 -7200
# Node ID 68b615bc110ed410992c2bea520d89a719b3c2eb
# Parent  4f1a78454452349826a98066c54a0aa887cdba74
export intro_classes_tac;

diff -r 4f1a78454452 -r 68b615bc110e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Apr 26 19:53:19 2005 +0200
+++ b/src/Pure/axclass.ML	Tue Apr 26 19:55:25 2005 +0200
@@ -23,6 +23,7 @@
     -> thm list -> tactic option -> theory -> theory
   val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
   val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
+  val intro_classes_tac: thm list -> tactic
   val default_intro_classes_tac: thm list -> tactic
   val axclass_tac: thm list -> tactic
   val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T