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