src/Pure/axclass.ML
changeset 16333 490d77820631
parent 16180 a51be5cbd81d
child 16364 dc9f7066d80a
     1.1 --- a/src/Pure/axclass.ML	Thu Jun 09 12:03:19 2005 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu Jun 09 12:03:20 2005 +0200
     1.3 @@ -9,17 +9,17 @@
     1.4  sig
     1.5    val quiet_mode: bool ref
     1.6    val print_axclasses: theory -> unit
     1.7 -  val add_axclass: bclass * xclass list -> ((bstring * string) * Attrib.src list) list
     1.8 +  val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list
     1.9      -> theory -> theory * {intro: thm, axioms: thm list}
    1.10 -  val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
    1.11 +  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list
    1.12      -> theory -> theory * {intro: thm, axioms: thm list}
    1.13    val add_classrel_thms: thm list -> theory -> theory
    1.14    val add_arity_thms: thm list -> theory -> theory
    1.15 -  val add_inst_subclass: xclass * xclass -> tactic -> theory -> theory
    1.16 +  val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
    1.17    val add_inst_subclass_i: class * class -> tactic -> theory -> theory
    1.18    val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
    1.19    val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
    1.20 -  val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
    1.21 +  val instance_subclass_proof: xstring * xstring -> bool -> theory -> ProofHistory.T
    1.22    val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
    1.23    val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
    1.24    val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
    1.25 @@ -28,7 +28,7 @@
    1.26  
    1.27    (*legacy interfaces*)
    1.28    val axclass_tac: thm list -> tactic
    1.29 -  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
    1.30 +  val add_inst_subclass_x: xstring * xstring -> string list -> thm list
    1.31      -> tactic option -> theory -> theory
    1.32    val add_inst_arity_x: xstring * string list * string -> string list
    1.33      -> thm list -> tactic option -> theory -> theory