export intro_classes_tac;
authorwenzelm
Tue Apr 26 19:55:25 2005 +0200 (2005-04-26 ago)
changeset 1585368b615bc110e
parent 15852 4f1a78454452
child 15854 1ae0a47dcccd
export intro_classes_tac;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 26 19:53:19 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 26 19:55:25 2005 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4      -> thm list -> tactic option -> theory -> theory
     1.5    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
     1.6    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
     1.7 +  val intro_classes_tac: thm list -> tactic
     1.8    val default_intro_classes_tac: thm list -> tactic
     1.9    val axclass_tac: thm list -> tactic
    1.10    val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T