More functions are added to the signature of ResClause
authormengj
Wed, 19 Oct 2005 13:59:33 +0200
changeset 17908 ac97527724ba
parent 17907 c20e4bddcb11
child 17909 7540483e9228
More functions are added to the signature of ResClause
src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Oct 19 10:25:46 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Wed Oct 19 13:59:33 2005 +0200
@@ -48,6 +48,19 @@
   val const_prefix : string
   val tconst_prefix : string 
   val class_prefix : string 
+
+  val union_all : ''a list list -> ''a list
+  val ascii_of : String.string -> String.string
+  val paren_pack : string list -> string
+  val bracket_pack : string list -> string
+  val make_schematic_var : String.string * int -> string
+  val make_fixed_var : String.string -> string
+  val make_schematic_type_var : string * int -> string
+  val make_fixed_type_var : string -> string
+  val make_fixed_const : String.string -> string		
+  val make_fixed_type_const : String.string -> string   
+  val make_type_class : String.string -> string
+
   end;
 
 structure ResClause: RES_CLAUSE =