More functions are added to the signature of ResClause
authormengj
Wed Oct 19 13:59:33 2005 +0200 (2005-10-19)
changeset 17908ac97527724ba
parent 17907 c20e4bddcb11
child 17909 7540483e9228
More functions are added to the signature of ResClause
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Oct 19 10:25:46 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 19 13:59:33 2005 +0200
     1.3 @@ -48,6 +48,19 @@
     1.4    val const_prefix : string
     1.5    val tconst_prefix : string 
     1.6    val class_prefix : string 
     1.7 +
     1.8 +  val union_all : ''a list list -> ''a list
     1.9 +  val ascii_of : String.string -> String.string
    1.10 +  val paren_pack : string list -> string
    1.11 +  val bracket_pack : string list -> string
    1.12 +  val make_schematic_var : String.string * int -> string
    1.13 +  val make_fixed_var : String.string -> string
    1.14 +  val make_schematic_type_var : string * int -> string
    1.15 +  val make_fixed_type_var : string -> string
    1.16 +  val make_fixed_const : String.string -> string		
    1.17 +  val make_fixed_type_const : String.string -> string   
    1.18 +  val make_type_class : String.string -> string
    1.19 +
    1.20    end;
    1.21  
    1.22  structure ResClause: RES_CLAUSE =