(* Title: MiniML/Type.thy Author: Wolfgang Naraschewski and Tobias Nipkow Copyright 1996 TU Muenchen *) section "MiniML-types and type substitutions" theory Type imports Maybe begin ― ‹type expressions› datatype "typ" = TVar nat | Fun "typ" "typ" (infixr "->" 70) ― ‹type schemata›