src/Pure/General/long_name.ML
changeset 77964 d4184ea197ec
parent 77962 01e04f024bb5
child 77993 fdb71efcc04a
equal deleted inserted replaced
77963:3a97b5bff51a 77964:d4184ea197ec
    29   val base_chunks: string -> chunks
    29   val base_chunks: string -> chunks
    30   val suppress_chunks: int -> bool list -> string -> chunks
    30   val suppress_chunks: int -> bool list -> string -> chunks
    31   val make_chunks: string -> chunks
    31   val make_chunks: string -> chunks
    32   val explode_chunks: chunks -> string list
    32   val explode_chunks: chunks -> string list
    33   val implode_chunks: chunks -> string
    33   val implode_chunks: chunks -> string
    34   val compare_chunks: chunks * chunks -> order
    34   val compare_chunks: chunks ord
    35   val eq_chunks: chunks * chunks -> bool
    35   val eq_chunks: chunks * chunks -> bool
    36   structure Chunks: CHANGE_TABLE
    36   structure Chunks: CHANGE_TABLE
    37 end;
    37 end;
    38 
    38 
    39 structure Long_Name: LONG_NAME =
    39 structure Long_Name: LONG_NAME =