src/Pure/sign.ML
changeset 22811 eb59c9b76d52
parent 22796 34c316d7b630
child 22846 fb79144af9a3
     1.1 --- a/src/Pure/sign.ML	Thu Apr 26 14:24:13 2007 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Apr 26 14:24:14 2007 +0200
     1.3 @@ -23,11 +23,6 @@
     1.4    val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
     1.5    val add_consts: (bstring * string * mixfix) list -> theory -> theory
     1.6    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.7 -  val add_const_constraint: xstring * string option -> theory -> theory
     1.8 -  val add_const_constraint_i: string * typ option -> theory -> theory
     1.9 -  val primitive_class: string * class list -> theory -> theory
    1.10 -  val primitive_classrel: class * class -> theory -> theory
    1.11 -  val primitive_arity: arity -> theory -> theory
    1.12    val add_trfuns:
    1.13      (string * (ast list -> ast)) list *
    1.14      (string * (term list -> term)) list *
    1.15 @@ -178,6 +173,11 @@
    1.16    val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.17    val add_abbrev: string -> bstring * term -> theory -> (term * term) * theory
    1.18    include SIGN_THEORY
    1.19 +  val add_const_constraint: xstring * string option -> theory -> theory
    1.20 +  val add_const_constraint_i: string * typ option -> theory -> theory
    1.21 +  val primitive_class: string * class list -> theory -> theory
    1.22 +  val primitive_classrel: class * class -> theory -> theory
    1.23 +  val primitive_arity: arity -> theory -> theory
    1.24    val hide_classes: bool -> xstring list -> theory -> theory
    1.25    val hide_classes_i: bool -> string list -> theory -> theory
    1.26    val hide_types: bool -> xstring list -> theory -> theory