27 

    27 

    28   \item unification and typing algorithms 

    28   \item unification and typing algorithms 

    29   (@{ML_file "Pure/pattern.ML"} implements HOPU)

    29   (@{ML_file "Pure/pattern.ML"} implements HOPU)

    30 

    30 

    31   \item useful datastructures: discrimination nets, association lists

    31   \item useful datastructures: discrimination nets, association lists

    32   \end{itemize}

    34   \end{itemize}

    33 *}

    35 *}

    34 

    36 

    35 end

    37 end