exported 'cat';
authorwenzelm
Mon, 14 Nov 1994 11:57:32 +0100
changeset 710 53fef17a729a
parent 709 0d0df9b5afe3
child 711 bb868a30e66f
exported 'cat';
src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Mon Nov 14 10:49:39 1994 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Mon Nov 14 11:57:32 1994 +0100
@@ -58,6 +58,7 @@
   val pure_sections:
     (string * (token list -> (string * string) * token list)) list
   (*items for building strings*)
+  val cat: string -> string -> string
   val parens: string -> string
   val brackets: string -> string
   val mk_list: string list -> string