changeset 710 | 53fef17a729a |
parent 656 | ec05d2fdfeee |
child 759 | e0b172d01c37 |
--- 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